X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FPOPLmark%2FFsub%2Fpart1a.ma;h=f38b5b332f682cffd2357e9bbef6a619b05133a4;hb=3fb8cc2606e15f256f93c653b5136f609b385208;hp=b113769ddf042c01de9461b28df7fe999692cdbc;hpb=233826389b4c0c4192c1eb1cacc8cfa99b2750f4;p=helm.git

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma
index b113769dd..f38b5b332 100644
--- a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma
@@ -14,8 +14,6 @@
 
 include "Fsub/defn.ma".
 
-axiom daemon : False.
-
 (*** Lemma A.1 (Reflexivity) ***)
 theorem JS_Refl : ∀T,G.WFType G T → WFEnv G → G ⊢ T ⊴  T.
 intros 3; elim H;