proposition: Lemma RL_sub_SS : forall i : nat, sub i <= S (pred (sub (S i))).
proof: Proof. intro; cut (sub i < sub (S i)); [ intro | apply H0 ]. rewrite (Nat.lt_succ_pred _ _ H1); apply Nat.lt_le_incl; apply H0. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef