X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FPOPLmark%2FFsub%2Fpart1a.ma;h=74ba49240cbe06f6169109e1144c2baaa60a222b;hb=56c4e355b88aa505b64c539053aba92eb86afc2a;hp=9e097b279cab5a032eea7735d1b334a5c471ff28;hpb=9883f04161a9972f0641dd85faf224b4f2846f05;p=helm.git

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma
index 9e097b279..74ba49240 100644
--- a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma
@@ -16,9 +16,8 @@ include "Fsub/defn.ma".
 
 (*** Lemma A.1 (Reflexivity) ***)
 theorem JS_Refl : ∀T,G.(G ⊢ T) → G ⊢ ♦ → G ⊢ T ⊴  T.
-intros 3; elim H;
- [1,2,3: autobatch
- | apply SA_All; [ autobatch | intros;autobatch depth=4 size=10]]
+intros 3; elim H;try autobatch;
+apply SA_All; [ autobatch | intros;autobatch depth=4 size=10]
 qed.
 
 (*
@@ -28,10 +27,9 @@ qed.
  *)
 
 lemma JS_weakening : ∀G,T,U.G ⊢ T ⊴ U → ∀H.H ⊢ ♦ → G ⊆ H → H ⊢ T ⊴ U.
-intros 4; elim H;
- [1,2,3,4: autobatch depth=4 size=7
- | apply (SA_All ? ? ? ? ? (H2 ? H6 H7));
-   intros; apply H4;autobatch depth=4 size=7]
+intros 4; elim H;try autobatch depth=4 size=7;
+apply (SA_All ? ? ? ? ? (H2 ? H6 H7));
+intros; autobatch depth=6 width=4 size=13;
 qed.
 
 inverter JS_indinv for JSubtype (%?%).
@@ -58,7 +56,7 @@ lemma JS_trans_prova: ∀T,G1.(G1 ⊢ T) →
 intros 3;elim H;clear H;
   [elim H3 using JS_indinv;destruct;autobatch
   |inversion H3; intros; destruct; assumption
-  |*: elim H6 using JS_indinv;destruct;
+  |*:elim H6 using JS_indinv;destruct;
     [1,3: autobatch
     |*: inversion H7; intros; destruct;
       [1,2: autobatch depth=4 width=4 size=9
@@ -84,4 +82,4 @@ theorem JS_narrow : ∀G1,G2,X,P,Q,T,U.
                        G2 @ !X ⊴ P :: G1 ⊢ T ⊴ U.
 intros;apply (narrowing ? ? ? ? ? ? ? H1 ? H) [|autobatch]
 intros;apply (JS_trans ? ? ? ? ? H2);apply (JS_weakening ? ? ? H1);autobatch.
-qed.
+qed.
\ No newline at end of file