theorem insert_conf: \forall P,Q1,S1,i1. Insert S1 i1 P Q1 \to
\forall Q2,S2,i2. Insert S2 i2 P Q2 \to
\exists Q,j1,j2.
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
theorem insert_conf: \forall P,Q1,S1,i1. Insert S1 i1 P Q1 \to
\forall Q2,S2,i2. Insert S2 i2 P Q2 \to
\exists Q,j1,j2.
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