The Coq mailing list

[Jeffrey Terrell <jeffrey.terrell AT kcl.ac.uk>]

In f, are X and X0 the same set?

Inductive T : Set -> Type :=
   Build_T : forall X : Set, T X.

Definition f (X : Set) (t : T X) (x : X) :=
   match t with Build_T X0 => forall x0 : X0, x = x0 end.

If they are, why does Coq reject the expression x = x0?

If they're not, how are they related?

Thanks. Jeff.