proposition: Theorem doTripletEqMonotone : forall (S1 S2 S3 S4 : State) (t : triplet), doTripletP S1 t S3 -> doTripletP S2 t S4 -> inclState S1 S2 -> inclState S3 S4.
proof: Proof. intros S1 S2 S3 S4 t H' H'0 H'1. elim (doTripletMonotoneEx S1 S2 S3 t); [ intros S5 E; Elimc E; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. apply inclStateEqStateComp with (S1 := S3) (S3 := S5); auto with stalmarck. apply doTripletEq with (S1 := S2) (t := t); auto with stalmarck. Qed.