The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Only tangentially related to the original discussion but:

AFAIK, there is no "erewrite ... with (var := value)" like there is
for "eapply".

 

Hugo Herbelin pointed out to me, the other day, that erewrite indeed supports "with" bindings:

Goal forall (P Q:nat->Type), (forall (x y:nat), P x = Q y) -> forall x, P x.
Proof.
  intros * h *.
  rewrite h with (y:=x).

When rewriting with several lemmas, one with is allowable per lemma:

Goal forall (P Q T:nat->Type), (forall (x y:nat), P x = Q y) -> (forall (x y:nat), T x = Q y) -> forall x, P x.
Proof.
  intros * h p *.
  rewrite h with (y:=x), <- p with (x:=x).

Hope this is useful.