proposition: Theorem doTripletIncl : forall (S1 S2 : State) (t : triplet), doTripletP S1 t S2 -> inclState S1 S2.
proof: Proof. intros S1 S2 t H'. case (doTripletUnionEx S1 S2 t); auto with stalmarck. intros x H'0; rewrite H'0; auto with stalmarck. Qed.