proposition: Theorem doTripletsMonotoneEx : forall (S1 S2 S3 : State) (L : list triplet), doTripletsP S1 L S3 -> inclState S1 S2 -> exists S4 : State, doTripletsP S2 L S4 /\ inclState S3 S4.
proof: Proof. intros S1 S2 S3 L H' H'0. lapply (doTripletCongruent S1 S3 S2 L); [ intros H'5 | idtac ]; auto with stalmarck. exists (unionState S2 S3); split; auto with stalmarck. apply doTripletsComp with (S1 := unionState S2 S1) (S2 := unionState S2 S3); auto with stalmarck. red in |- *; split; auto with stalmarck. Qed.
imports: Stalmarck(PolyListAux)