The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

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