]> matita.cs.unibo.it Git - helm.git/commitdiff
Remove the daemon :-)
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 17 Jun 2011 10:22:29 +0000 (10:22 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 17 Jun 2011 10:22:29 +0000 (10:22 +0000)
matita/matita/lib/basics/jmeq.ma

index ad3aa937101c238a90ab7ac0ad921e357d1776b0..9f2d758c158bf3810ca85ab8cb5bc8bf04a37036 100644 (file)
@@ -51,8 +51,6 @@ lemma gral: ∀A.∀x,y:A.
  #H @H
 qed.
 
-axiom daemon: False.
-
 lemma jm_to_eq_sigma:
  ∀A,x,y. jmeq A x A y → mk_Sigma A x = mk_Sigma A y.
  #A #x #y #E cases E in ⊢ (???%); %