proposition: Theorem doTripletEqAux2 : forall (p q r s : rZ) (S1 S3 : State) (t : triplet), doTripletP S1 t (addEq (p, q) (addEq (r, s) S1)) -> eqState S1 S3 -> doTripletP S3 t (addEq (p, q) (addEq (r, s) S3)) -> ex (fun S4 : State => doTripletP S3 t S4 /\ eqState S4 (addEq (p, q) (addEq (r, s) S1))).
proof: Proof. intros p q r s S1 S3 t H' H'0; exists (addEq (p, q) (addEq (r, s) S3)); split; auto with stalmarck. Qed.