The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Edsko de Vries wrote:
> Thanks for taking the time to reply. However, I'm not sure your answer 
> generalizes to the real proof I'm attempting, since you are taking 
> advantage of the fact that I only introduced one constructor for T.

Here's a proof of [bar] that uses your [a_is_b]:

Lemma bar : X (U + 1 - 1) b = X U a.
 generalize a_is_b; generalize b; rewrite foo;
   intros; match goal with
             | [ H : _ |- _ ] => rewrite H
           end; reflexivity.
Qed.