The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 05/15/2012 05: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), ....
>    

Your schematic example doesn't quite tell me which pattern you're aiming 
for, but here's a simple definition that at least captures a related 
pattern:

Fixpoint identities (A : Type) (n : nat) : Prop :=
  match n with
    | O => True
    | S n' => forall (x y : A), identities (x = y) n'
  end.

Eval compute in identities nat 4.