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