(*** 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.
(*
*)
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 (%?%).
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
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