include "metrics/Prod_Sub.ma".
(* UNEXPORTED
-Section lists.
+Section lists
*)
(*#* **Lists
inline "cic:/CoRN/metrics/CPMSTheory/map_member.con".
(* UNEXPORTED
-End lists.
+End lists
*)
(* UNEXPORTED
-Section loc_and_bound.
+Section loc_and_bound
*)
(*#* **Pseudo Metric Space theory
inline "cic:/CoRN/metrics/CPMSTheory/well_contained.con".
(* UNEXPORTED
-End loc_and_bound.
+End loc_and_bound
*)