proposition: Theorem doTripletUnionAux1 : forall (p q : rZ) (S1 S3 : State) (t : triplet), doTripletP (unionState S3 S1) t (addEq (p, q) (unionState S3 S1)) -> exists S4 : State, doTripletP (unionState S3 S1) t S4 /\ eqState S4 (unionState S3 (addEq (p, q) S1)).
proof: Proof. intros p q S1 S3 t H'; exists (addEq (p, q) (unionState S3 S1)); split; auto with stalmarck. apply eqStateTrans with (unionState (unionState ((p, q) :: nil) S3) S1); auto with stalmarck. apply eqStateTrans with (unionState (unionState S3 ((p, q) :: nil)) S1); auto with stalmarck. apply eqStateSym; auto with stalmarck. replace (addEq (p, q) S1) with (unionState ((p, q) :: nil) S1); auto with stalmarck. apply unionStateAssoc; auto with stalmarck. Qed.