The Coq mailing list

[Cody Roux <Cody.Roux AT loria.fr>]

On Tue, 2009-10-20 at 12:24 -0400, Vladimir Voevodsky wrote:
> Given an inductive type such as
> 
> Inductive two_el := el_1 | el_2 .
> 
> are there closed terms of type two_el which do not reduce to either  
> el_1 or el_2 ?

No. This can be deduced from the strong normalisation property of the
underlying calculus of Coq (CIC+Predicative Set+Universes), combined
with the Inversion Property: It is easy to show by case analysis that
any term in normal form and in the empty context of type two_el must be
one of the constructors of this type. This can be compared with the
disjunction property which states:

If t is a term of type A\/B in the empty context then t reduces to
inl t1   or to    inr t2

Which happens to be quite a desirable property in constructive
mathematics.

Cheers

Cody