qed.
theorem insert_inv_succ: \forall S,Q1,Q2,i. Insert S (succ i) Q1 Q2 \to
\exists P1,P2,R. Insert S i P1 P2 \land
Q1 = abst P1 R \land Q2 = abst P2 R.
qed.
theorem insert_inv_succ: \forall S,Q1,Q2,i. Insert S (succ i) Q1 Q2 \to
\exists P1,P2,R. Insert S i P1 P2 \land
Q1 = abst P1 R \land Q2 = abst P2 R.