- xoa: more existential types

[helm.git] / matita / matita / lib / basics / jmeq.ma

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