proposition: Theorem doTripletInvolEx : forall (t : triplet) (S1 S2 S3 : State), doTripletP S1 t S2 -> inclState S2 S3 -> exists S4 : State, doTripletP S3 t S4 /\ eqState S3 S4.
proof: Proof. intros t S1 S2 S3 H' H'0; (generalize (eqStateIncl S1); intros Eq0); cut (inclState S1 S3); [ idtac | apply inclStateTrans with (S2 := S2); auto with stalmarck; apply doTripletIncl with (t := t); auto with stalmarck ]; generalize H'0; clear H'0; elim H'; intros p q r H'0 H'1 H'2; apply doTripletInvolExAux2 with (1 := H'1) || apply doTripletInvolExAux1 with (1 := H'1); auto with stalmarck. Qed.