proposition: Lemma RL_sub_mon : forall i j : nat, i < j -> sub i < sub j.
proof: Proof. elim (proj2a_sig2T _ _ _ Href); intros. elim H0; intros. elim H1; auto. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef