X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Fjmeq.ma;h=9f2d758c158bf3810ca85ab8cb5bc8bf04a37036;hb=7b1406845cc6a9885114c8be79224f2b0a17d700;hp=ad3aa937101c238a90ab7ac0ad921e357d1776b0;hpb=53452958508001e7af3090695b619fe92135fb9e;p=helm.git

diff --git a/matita/matita/lib/basics/jmeq.ma b/matita/matita/lib/basics/jmeq.ma
index ad3aa9371..9f2d758c1 100644
--- a/matita/matita/lib/basics/jmeq.ma
+++ b/matita/matita/lib/basics/jmeq.ma
@@ -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 ⊢ (???%); %