set "baseuri" "cic:/matita/CoRN-Decl/metrics/Equiv".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: Equiv.v,v 1.4 2004/04/23 10:01:02 lcf Exp $ *)
include "metrics/IR_CPMSpace.ma".
(* UNEXPORTED
-Section equivalent.
+Section equivalent
*)
(*#* **Equivalent Pseudo Metric Spaces
inline "cic:/CoRN/metrics/Equiv/MSequivalent_discr.con".
(* UNEXPORTED
-End equivalent.
+End equivalent
*)