-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;