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