huge commit in automation:

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

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma
index 5a472e640ca11bfb9cd8bb06f8aaeb04a7c34577..c1e9090974efb131486b0017b49c1ac1e377743f 100644 (file)
--- a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion.ma
@@ -22,7 +22,8 @@ intros 3.elim H
   |apply (SA_Arrow ? ? ? ? ? (H2 H5) (H4 H5))
   |apply (SA_All ? ? ? ? ? (H2 H5));intros;apply (H4 ? H6)
      [intro;apply H6;apply (fv_WFT ? ? ? (WFT_Forall ? ? ? H1 H3));
-      simplify;autobatch
+      simplify;
+      autobatch; 
      |autobatch]]
 qed.