Wed Jun 1 11:26:49 EEST 2011

Coq nonsense

Coq nonsense Critical systems use warez like this. 
Definition tr1(t:True) : Prop :=False.
Coercion tr1: True >-> Sortclass.

Lemma FUCKMS: forall a : True, a->False.
Proof.
compute. firstorder.
Qed.

Posted by joro | Permanent link
/\