proposition: Theorem doTripletInvolExAux2 : forall (tr : triplet) (p q r s : rZ) (S1 S3 : State), inclState (addEq (p, q) (addEq (r, s) S1)) S3 -> inclState S1 S3 -> doTripletP S3 tr (addEq (p, q) (addEq (r, s) S3)) -> ex (fun S4 : State => doTripletP S3 tr S4 /\ eqState S3 S4).
proof: Proof. intros tr p q r s S1 S3 H' H'0 H'1; exists (addEq (p, q) (addEq (r, s) S3)); split; auto with stalmarck. generalize (eqStateIncl (addEq (p, q) (addEq (r, s) S1))); intros Eq1; red in |- *; auto 8 with stalmarck. Qed.