proposition: Theorem vallStateLe : forall S1 S2 : State, inclState S1 S2 -> valState S2 <= valState S1.
proof: Proof. unfold valState in |- *; auto with stalmarck. Qed.
imports: Stalmarck(state) Coq(Arith) Stalmarck(stateDec) Coq(Inverse_Image) Coq(Compare) Coq(Relation_Definitions)