improve error messages for `apply` and similar transformations
On example
predicate p int int
axiom A: forall x:int. p x x
goal g: p 42 43
The use of apply A
produces the error:
Error in transformation apply during unification of following two terms:
x : int
42 : int
which is misleading: there is no reason why x
could not unify with 42
. It should explain that x
is already matched with 43
.