proposition: Theorem doTripletEqCompEx : forall (S1 S2 S3 : State) (t : triplet), doTripletP S1 t S2 -> eqState S1 S3 -> exists S4 : State, doTripletP S3 t S4 /\ eqState S4 S2.
proof: Proof. intros S1 S2 S3 t H' H'1; inversion H'; apply doTripletEqAux2 || apply doTripletEqAux1; auto with stalmarck; generalize (eqStateEq _ _ _ _ H'1 H); auto with stalmarck. Qed.