The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

How about 


Definition eqnplus1 ( n:nat ) {X : Type} ( x y : X) : Type.
Proof. here follow the "destruct n" with eq X x y for n=0 and the obvious 
step for n+1. Defined.



V.




On May 15, 2012, at 5:28 PM, Andrej Bauer wrote:

> I am trying to formalize arguments in Coq which use arbitrarily nested
> identity types, i.e., I want to write things like:
> 
>  forall (x0 y0 : A) (x1 y1 : x0 = y0) (x2 y2 : x1 = y1) ... (xn yn :
> x(n-1) = y(n-1), ....
> 
> What is the best way to organize things here? Typically, I need access
> to the highest-level term xn yn, and typically I need to show
> something for every level n of nesting.
> 
> Some sort of magic involving Inductive or Fixpoint is called for. The
> above nested forall could be replaced, e.g., by something like
> 
>  forall (p q : eq' n), ...
> 
> where eq' n is the n-th iterated identity type. But not quite. Help!
> 
> With kind regards,
> 
> Andrej