Transformation `rewrite` produces confusing error message
In the example
use int.Int
predicate p int
function f int : int
axiom H : forall x y. p y -> y >= f x -> f (x+1) = f x + 1
goal G : p (f (42+1))
apply rewrite H
produces the message
rewrite: no term matching the given pattern
which is not the right error message, it should say that the value of y
should be given using with