inline "cic:/CoRN/reals/CReals1/Lim_seq_eq_Lim_subseq.con".
inline "cic:/CoRN/reals/CReals1/Lim_subseq_eq_Lim_seq.con".
(* UNEXPORTED
inline "cic:/CoRN/reals/CReals1/Lim_seq_eq_Lim_subseq.con".
inline "cic:/CoRN/reals/CReals1/Lim_subseq_eq_Lim_seq.con".
(* UNEXPORTED