- replaced part1a/defn with the version based on induction/inversion and deleted

[helm.git] / helm / software / matita / contribs / POPLmark / Fsub / part1a.ma

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma
index b113769ddf042c01de9461b28df7fe999692cdbc..f38b5b332f682cffd2357e9bbef6a619b05133a4 100644 (file)
--- 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;