From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 1 Jun 2009 12:23:46 +0000 (+0000)
Subject: This works for me
X-Git-Tag: make_still_working~3935
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fcda9a37eb169fbd3dcf1b2ed699cf8444b4d714;p=helm.git

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 14f1525a7..234c6aa39 100644
--- 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;