proposition: Theorem stalmarckUnionEx : forall (S1 S2 : State) (L : list triplet), stalmarckP S1 L S2 -> exists S3 : State, eqState S2 (unionState S3 S1).
proof: Proof. intros S1 S2 L H'; Elimc H'; clear L S1 S2; auto with stalmarck. exact doTripletsUnionEx. intros a b S1 S2 S3 S4 L H' H'0 H'1 H'2 H'3; exists S4; auto with stalmarck. red in |- *; split; auto with stalmarck. apply unionStateMin; auto with stalmarck. apply inclStateEqStateComp with (S1 := S1) (S3 := interState S2 S3); auto with stalmarck. apply interMemMin; auto with stalmarck. Elimc H'0; intros S5 E. apply inclStateEqStateComp with (S1 := S1) (S3 := unionState (unionState S5 (addEq (a, b) nil)) S1); auto with stalmarck. apply eqStateTrans with (S2 := unionState S5 (unionState (addEq (a, b) nil) S1)); auto with stalmarck. apply eqStateSym; auto with stalmarck. apply unionStateAssoc; auto with stalmarck. Elimc H'2; intros S5 E. apply inclStateEqStateComp with (S1 := S1) (S3 := unionState (unionState S5 (addEq (a, rZComp b) nil)) S1); auto with stalmarck. apply eqStateTrans with (S2 := unionState S5 (unionState (addEq (a, rZComp b) nil) S1)); auto with stalmarck. apply eqStateSym; auto with stalmarck. apply unionStateAssoc; auto with stalmarck. intros S1 S2 S3 L H' H'0 H'1 H'2. elim H'0; intros S4 E; clear H'0. elim H'2; intros S5 E0; clear H'2. exists (unionState S5 S4); auto with stalmarck. apply eqStateTrans with (S2 := unionState S5 (unionState S4 S1)); auto with stalmarck. apply eqStateTrans with (S2 := unionState S5 S2); auto with stalmarck. apply unionStateAssoc; auto with stalmarck. Qed.