- Procedural: now we generate the exact tactic (in place of some apply tactics) and...

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

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion2.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion2.ma
index a8dd6370fc559de5cd4d910ee73510a998e0c492..a9ad6d28d2db057d7205067c662b288cfcc0e031 100644 (file)
--- a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion2.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion2.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Fsub/defn.ma".
+include "Fsub/defn2.ma".
 
 (*** Lemma A.1 (Reflexivity) ***)
 theorem JS_Refl : ∀T,G.WFType G T → WFEnv G → G ⊢ T ⊴  T.
@@ -110,7 +110,8 @@ qed.
 lemma JS_trans_prova: ∀T,G1.WFType G1 T →
 ∀G,R,U.incl ? (fv_env G1) (fv_env G) → G ⊢ R ⊴ T → G ⊢ T ⊴ U → G ⊢ R ⊴ U.
 intros 3;elim H;clear H; try autobatch;
-  [rewrite > (JSubtype_Top ? ? H3); autobatch
+  [ apply (JSubtype_inv ? ? ? ? ? ? ? ? ? H3); intros; destruct; autobatch
+  | inversion H3; intros; destruct; assumption
   |*: apply (JSubtype_inv ? ? ? ? ? ? ? ? ? H6); intros; destruct;
     [1,3: autobatch
     |*: inversion H7; intros; destruct;
@@ -124,20 +125,20 @@ intros 3;elim H;clear H; try autobatch;
       | apply SA_All
          [ autobatch
          | intros;apply (H4 X);
-            [intro;apply H13;apply H5;assumption
-                |intro;apply H13;apply H5;apply (WFT_to_incl ? ? ? H3);
-                 assumption
-                |simplify;autobatch
-                |apply (narrowing X (mk_bound true X t::G) ? ? ? ? ? H9 ? ? [])
-                   [intros;apply H2
-                      [unfold;intros;lapply (H5 ? H15);rewrite > fv_append;
-                       autobatch
-                      |apply (JS_weakening ? ? ? H9)
-                         [autobatch
-                         |unfold;intros;autobatch]
-                      |assumption]
-                   |*:autobatch]
-                |autobatch]]]]]
+            [intro; autobatch;
+            |intro;  apply H13;apply H5; apply (WFT_to_incl ? ? ? H3);
+             assumption
+            |simplify;autobatch
+            |apply (narrowing X (mk_bound true X t::G) ? ? ? ? ? H9 ? ? [])
+               [intros;apply H2
+                  [unfold;intros;lapply (H5 ? H15);rewrite > fv_append;
+                   autobatch
+                  |apply (JS_weakening ? ? ? H9)
+                     [autobatch
+                     |unfold;intros;autobatch]
+                  |assumption]
+               |*:autobatch]
+            |autobatch]]]]]
 qed.
 
 theorem JS_trans : ∀G,T,U,V.G ⊢ T ⊴ U → G ⊢ U ⊴ V → G ⊢ T ⊴ V.