proposition: Theorem stalmarckInclList : forall (L1 L2 : list triplet) (S1 S2 : State), incl L1 L2 -> stalmarckP S1 L1 S2 -> stalmarckP S1 L2 S2.
proof: Proof. intros L1 L2 S1 S2 H' H'0; generalize L2 H'; clear H' L2; elim H'0; auto with stalmarck. intros S3 S4 L H' L2 H'1. apply stalmarckPref. apply doTripletsInclList with (L1 := L); auto with stalmarck. intros a b S3 S4 S5 S6 L H' H'1 H'2 H'3 H'4 L2 H'5. apply stalmarckPSplit with (a := a) (b := b) (S2 := S4) (S3 := S5); auto with stalmarck. intros S3 S4 S5 L H' H'1 H'2 H'3 L2 H'4. apply stalmarckTrans with (S2 := S4); auto with stalmarck. Qed.