The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

hugo.herbelin AT inria.fr
 wrote:
> On the other side, with Nat defined polymorphically in impredicative
> Set (with option -impredicative-set), you get a full recursor
> "Nat_rec" and at least the computational expressiveness of system T
> but you cannot derive 0<>1 (and the recursor has a bad complexity due
> to the linear complexity of the predecessor).
>   

Doesn't the unprovability of [0 <> 1] only arise from doing away with 
inductive types altogether?  If we just single out [nat] to be defined 
with impredicative polymorphism, then [0 <> 1] seems to reduce simply to 
[false <> true], which [discriminate] proves.