Error when matching same transformation with different number of arguments
When matching a session, a check is performed to see if the same transformation (with the same parameters) is already applied. This check goes wrong when a transformation is applied but with different number of arguments.
To reproduce, consider this example:
use int.Int
predicate p int
constant i : int
goal G : p i
Apply both induction i
and induction i from 1
to the task and then try to replay it.