proposition: Theorem doTripletsUnionEx : forall (S1 S2 : State) (L : list triplet), doTripletsP S1 L S2 -> exists S3 : State, eqState S2 (unionState S3 S1).
proof: Proof. intros S1 S2 L H'; elim H'; auto with stalmarck. intros S3 S4 H'0 H'1; exists S3; auto with stalmarck. apply eqStateTrans with (S2 := S3); auto with stalmarck. red in |- *; split; auto with stalmarck. intros S3 S4 S5 L0 t H'0 H'1 H'2 H'3. elim (doTripletUnionEx S3 S4 t); [ intros S6 E | idtac ]; auto with stalmarck. elim H'3; intros S7 E0. exists (unionState S7 S6). apply eqStateTrans with (S2 := unionState S7 S4); auto with stalmarck. rewrite E; auto with stalmarck. apply unionStateAssoc; auto with stalmarck. Qed.
imports: Stalmarck(PolyListAux)