Ssreflect Users Discussion List

[Guillaume Melquiond <>]

Hi,

Enrico feels the following should be made known to more people, so here
it is.

Have you ever wanted to rewrite using wildcards not only on the
left-hand side but also on the right-hand side of an equality? Are you
using Coq 8.5? Then the following trick might be of help to you:

Lemma foo x y : x + 3 + y = 3 + x + y.
rewrite (_ : ?[n] + 3 = 3 + ?n).

Best regards,

Guillaume