proposition: Theorem doTripletCongruentEx : forall (S1 S2 S3 : State) (t : triplet), doTripletP S1 t S2 -> exists S4 : State, doTripletP (unionState S3 S1) t S4 /\ eqState S4 (unionState S3 S2).
proof: Proof. intros S1 S2 S3 t H'; inversion H'; apply doTripletUnionAux2 || apply doTripletUnionAux1; auto with stalmarck; generalize (eqStateIncl _ _ _ _ (unionStateInclR S3 S1) H); auto with stalmarck. Qed.