The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

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 ?

That depends on the axioms that you assert.  With no axioms, I believe 
the CIC consistency theorem guarantees the property you describe (modulo 
differences between the real Coq implementation and the theory).

The axiom from the [Eqdep] module is a good example of a term that can 
block complete reduction, but is very useful.  There is also the less 
interesting case of trying to reduce terms that contain subterms marked 
as opaque with [Qed] or similar.