Fix : wrong exception was catch in apply_subst

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

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma
index 0f32da3495a805abaf39e369fce863957393c3e2..234c6aa3935008eba7833c5f842d34d5aee608df 100644 (file)
--- a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma
@@ -50,7 +50,7 @@ lemma JSubtype_inv:
  intros;
  generalize in match (refl_eq ? T);
  generalize in match (refl_eq ? G);
- elim H5 in ⊢ (? ? ? % → ? ? ? % → %); destruct; autobatch depth=3 width=4 size=7;
+ elim H5 in ⊢ (? ? ? % → ? ? ? % → %); destruct; autobatch width=4 size=7;
 qed.
 
 theorem narrowing:∀X,G,G1,U,P,M,N.
@@ -62,8 +62,7 @@ intros 10.elim H2; destruct;
  | elim (decidable_eq_nat X n)
     [apply (SA_Trans_TVar ? ? ? P); destruct;
       [ autobatch
-      | rewrite > append_cons; apply H1;
-        lapply (WFE_bound_bound true X t1 U ? ? H3); destruct;autobatch]
+      | lapply (WFE_bound_bound true X t1 U ? ? H3); autobatch]
     | apply (SA_Trans_TVar ? ? ? t1); autobatch]
  | autobatch
  | apply SA_All;
@@ -82,22 +81,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.