From 47070cf066ae366ac7f3e73594f1bc02b0efb7f4 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 13 May 2009 09:37:51 +0000
Subject: [PATCH] Sempre piu' breve

---
 .../POPLmark/Fsub/part1a_inversion3.ma         | 18 +++++-------------
 1 file changed, 5 insertions(+), 13 deletions(-)

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma
index 0f32da349..be3033199 100644
--- 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.
-- 
2.39.2