proposition: Theorem oneStateAllLe : forall (a b : rNat) (S1 S2 : State), inclState S1 S2 -> oneStateAll S2 a b <= oneStateAll S1 a b.
proof: Proof. intros a b S1 S2 H'; unfold oneStateAll in |- *; generalize oneStateLe; intros H'1; auto with stalmarck. Qed.
imports: Stalmarck(state) Coq(Arith) Stalmarck(stateDec) Coq(Inverse_Image) Coq(Compare) Coq(Relation_Definitions)