The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi Adam,

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.  
Suppose that we change the definition of T to

Inductive T : nat -> Set :=
 | MkT : forall (n:nat), T n
 | MkT2 : forall (n:nat), T n.

Trying this, I now also get stuck in my a_is_b lemma :-( Surely I  
should still be able to prove that a = b and that X U a = X (U + 1 -  
1) b?

Edsko