proposition: Theorem doTripletUnionEx : forall (S1 S2 : State) (t : triplet), doTripletP S1 t S2 -> exists S3 : State, S2 = unionState S3 S1.
proof: Proof. intros S1 S2 t H'; inversion H'; apply doTripletUnionEx2 with (t := t) || apply doTripletUnionEx1 with (t := t); auto with stalmarck; rewrite H1; auto with stalmarck. Qed.