Insert S2 j2 Q1 Q \land Insert S1 j1 Q2 Q.
intros 5. elim H; clear H i1 P Q1;
[ elim H1; clear H1 i2 c Q2; decompose; autobatch depth = 7 size = 8
Insert S2 j2 Q1 Q \land Insert S1 j1 Q2 Q.
intros 5. elim H; clear H i1 P Q1;
[ elim H1; clear H1 i2 c Q2; decompose; autobatch depth = 7 size = 8