The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

> Following the arguments of my previous email, if we rewrite 
> (False->True2)=True2 in the inductive definition we would get
> Inductive True2:Prop:= I2: True2->True2.
> which is False when the original is True.
Very nice example but we should not misinterpret  this last point
in order to identify

Inductive True2:Prop:= I2: True2->True2.
with
Inductive True2:Prop:= I2: (False -> True2)->True2.

you need (False -> X) = X forall X (which is not provable when X is 
False) and not just False -> True2 = True2
because the name is bound in the inductive definition

so the problem is still the same around the elimination on Heq "

assume < is the structural order related to True2 generated by (forall 
y, f y < l2 f)

Fixpoint con (x:True2) :False :=
match x with
I2 f => con (match Heq with eq_refl => f end)
end.

The hypothesis
forall y, f y < x
we would like to prove

(match Heq in (False->True2=True2) return fun X _ => X with eq_refl => f 
end) < x

but eliminating Heq requires a generalisation

(match Heq in (False->True2=Z) return fun X _ => X with eq_refl => f 
end) < x

which is not well-typed.

This is this situation we need to detect and forbid.
The point being not to miss tricky situations

Christine