This works for me

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma
index 14f1525a7cbe64d1327660087d81488d1f8d88df..234c6aa3935008eba7833c5f842d34d5aee608df 100644 (file)
--- a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma
@@ -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,7 +81,7 @@ intros 3;elim H;clear H; try autobatch;
       [1,2: autobatch depth=4 width=4 size=9
       | apply SA_Top
          [ assumption
-         | apply WFT_Forall;intros;autobatch depth =4]
+         | apply WFT_Forall;intros;autobatch depth=4]
       | apply SA_All
          [ autobatch
          | intros;apply (H4 X);simplify;