-lemma JS_weakening : ∀G,T,U.G ⊢ T ⊴ U → ∀H.WFEnv H → incl ? 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]
+lemma JS_weakening : ∀G,T,U.G ⊢ T ⊴ U → ∀H.H ⊢ ♦ → G ⊆ H → H ⊢ T ⊴ U.
+intros 4; elim H;try autobatch depth=4 size=7;
+apply (SA_All ? ? ? ? ? (H2 ? H6 H7));
+intros; autobatch depth=6 width=4 size=13;