Sempre piu' breve

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma
index 0f32da3495a805abaf39e369fce863957393c3e2..be3033199032948abeb85873badc93cc76dca3a2 100644 (file)
--- a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma
@@ -82,22 +82,14 @@ intros 3;elim H;clear H; try autobatch;
       [1,2: autobatch depth=4 width=4 size=9
       | apply SA_Top
          [ assumption
-         | apply WFT_Forall;
-            [ autobatch
-            | intros;autobatch depth =4]]
+         | apply WFT_Forall;intros;autobatch depth =4]
       | apply SA_All
          [ autobatch
-         | intros;apply (H4 X);
-            [intro; autobatch 
-            |intro; autobatch depth=4.  
-            |simplify; autobatch
-            |apply (narrowing X (mk_bound true X t::G) ? ? ? ? ? H9 ? ? [])
-               [intros;apply H2
-                  [unfold;intros;lapply (H5 ? H15);rewrite > fv_append;autobatch
-                  |autobatch
-                  |assumption]
+         | intros;apply (H4 X);simplify;
+            [4: apply (narrowing X (mk_bound true X t::G) ? ? ? ? ? H9 ? ? [])
+               [intros;apply H2;try unfold;intros;autobatch; 
                |*:autobatch]
-            |autobatch]]]]]
+            |*: autobatch]]]]]
 qed.
 
 theorem JS_trans : ∀G,T,U,V.G ⊢ T ⊴ U → G ⊢ U ⊴ V → G ⊢ T ⊴ V.