The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Edsko de Vries wrote:
> I am stuck in a proof that involves a dependent rewrite (I think) -- I 
> need to rewrite two variables simulatenously in order to complete the 
> proof.

The standard trick for that is to use [generalize].


Lemma singleton : forall n (x y : T n), x = y.
destruct x; dependent inversion y; reflexivity.
Qed.

Hint Resolve singleton.

Lemma singleton_cong : forall n (x y : T n), X n x = X n y.
intros; f_equal; auto.
Qed.

Hint Resolve singleton_cong.

Lemma bar : X (U + 1 - 1) b = X U a.
generalize b; rewrite foo; auto.
Qed.