proposition: Theorem doTripletsInclList : forall (L1 L2 : list triplet) (S1 S2 : State), incl L1 L2 -> doTripletsP S1 L1 S2 -> doTripletsP S1 L2 S2.
proof: Proof. intros L1 L2 S1 S2 H' H'0; generalize L2 H'; elim H'0; clear H'0 H' L2; auto with stalmarck. intros S3 S4 S5 L0 t H' H'0 H'1 H'2 L2 H'3. apply doTripletsTrans with (S2 := S4) (t := t); auto with datatypes stalmarck. Qed.
imports: Stalmarck(PolyListAux)