proposition: Theorem doTripletMonotoneEx : forall (S1 S2 S3 : State) (t : triplet), doTripletP S1 t S3 -> inclState S1 S2 -> exists S4 : State, doTripletP S2 t S4 /\ inclState S3 S4.
proof: Proof. intros S1 S2 S3 t H' H'0. elim (doTripletCongruentEx S1 S3 S2 t); [ intros S4 E; Elimc E; intros H'6 H'7 | idtac ]; auto with stalmarck. elim (doTripletEqCompEx (unionState S2 S1) S4 S2 t); [ intros S5 E; Elimc E; intros H'9 H'10 | idtac | idtac ]; auto with stalmarck. exists S5; split; auto with stalmarck. apply inclStateTrans with (S2 := unionState S2 S3); auto with stalmarck. apply inclStateEqStateComp with (S1 := S4) (S3 := S4); auto with stalmarck. red in |- *; auto with stalmarck. Qed.