Return Styles: Pseud0ch, Terminal, Valhalla, NES, Geocities, Blue Moon. Entire thread

Hot stripping coqs

Name: Anonymous 2012-04-26 17:03

Hello proggers.

How do I discharge this goal in Coq?

Inductive type : nat -> Set := ctor : forall n, type n.
Goal forall n, type 0 <> type (S n).

Name: Anonymous 2012-04-27 3:34

>>3

Thanks anon, but I just can't find a similar property for type.

Newer Posts