A few lemmas about inclusion.

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

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma
index b538f4d3aff0ecbdbb1132f2f840eea3bc878619..c1e9090974efb131486b0017b49c1ac1e377743f 100644 (file)
--- a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/Fsub/part1a_inversion/".
 include "Fsub/defn.ma".
 
 (*** Lemma A.1 (Reflexivity) ***)
@@ -23,7 +22,8 @@ intros 3.elim H
   |apply (SA_Arrow ? ? ? ? ? (H2 H5) (H4 H5))
   |apply (SA_All ? ? ? ? ? (H2 H5));intros;apply (H4 ? H6)
      [intro;apply H6;apply (fv_WFT ? ? ? (WFT_Forall ? ? ? H1 H3));
-      simplify;autobatch
+      simplify;
+      autobatch; 
      |autobatch]]
 qed.