proposition: Theorem doTripletsIncl : forall (S1 S2 : State) (L : list triplet), doTripletsP S1 L S2 -> inclState S1 S2.
proof: Proof. intros S1 S2 L H'. elim (doTripletsUnionEx S1 S2 L); [ intros S3 E | idtac ]; auto with stalmarck. apply inclStateEqStateComp with (S1 := S1) (S3 := unionState S3 S1); auto with stalmarck. Qed.
imports: Stalmarck(PolyListAux)