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