proposition: Theorem doTripletUnionEx2 : forall (p q r s : rZ) (S1 : State) (t : triplet), doTripletP S1 t (addEq (p, q) (addEq (r, s) S1)) -> exists S3 : State, addEq (p, q) (addEq (r, s) S1) = unionState S3 S1.
proof: Proof. intros p q r s S1 t H'; exists ((p, q) :: (r, s) :: nil); auto with stalmarck. Qed.