proposition: Lemma RL_sub_mon' : forall i j : nat, i <= j -> sub i <= sub j.
proof: Proof. intros. elim (le_lt_eq_dec _ _ H); intro. apply Nat.lt_le_incl; apply RL_sub_mon; assumption. rewrite b0; apply le_n. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef