proposition: Theorem NrelLe : forall (L1 : list rNat) (a : rNat) (S1 S2 : State), inclState S1 S2 -> Nrel S2 a L1 <= Nrel S1 a L1.
proof: Proof. intros L1 a S1 S2 H'; elim L1; simpl in |- *; auto with stalmarck. Qed.
imports: Stalmarck(state) Coq(Arith) Stalmarck(stateDec) Coq(Inverse_Image) Coq(Compare) Coq(Relation_Definitions)