set "baseuri" "cic:/matita/CoRN-Decl/devel/loeb/per/lst2fun".
-inline cic:/CoRN/devel/loeb/per/lst2fun/F'.con.
+include "CoRN.ma".
-inline cic:/CoRN/devel/loeb/per/lst2fun/F.ind.
+inline "cic:/CoRN/devel/loeb/per/lst2fun/F'.con".
-inline cic:/CoRN/devel/loeb/per/lst2fun/to_nat.con.
+inline "cic:/CoRN/devel/loeb/per/lst2fun/F.ind".
+
+coercion cic:/matita/CoRN-Decl/devel/loeb/per/lst2fun/F_crr.con 0 (* compounds *).
+
+inline "cic:/CoRN/devel/loeb/per/lst2fun/to_nat.con".
(* UNEXPORTED
Implicit Arguments to_nat [n].
*)
-(* INCLUDE
-CSetoids
-*)
+coercion cic:/matita/CoRN-Decl/devel/loeb/per/lst2fun/to_nat.con 0 (* compounds *).
+
+include "algebra/CSetoids.ma".
-inline cic:/CoRN/devel/loeb/per/lst2fun/Feq.con.
+inline "cic:/CoRN/devel/loeb/per/lst2fun/Feq.con".
-inline cic:/CoRN/devel/loeb/per/lst2fun/Fap.con.
+inline "cic:/CoRN/devel/loeb/per/lst2fun/Fap.con".
-inline cic:/CoRN/devel/loeb/per/lst2fun/Fap_irreflexive.con.
+inline "cic:/CoRN/devel/loeb/per/lst2fun/Fap_irreflexive.con".
-inline cic:/CoRN/devel/loeb/per/lst2fun/Fap_symmetric.con.
+inline "cic:/CoRN/devel/loeb/per/lst2fun/Fap_symmetric.con".
-inline cic:/CoRN/devel/loeb/per/lst2fun/Fap_cotransitive.con.
+inline "cic:/CoRN/devel/loeb/per/lst2fun/Fap_cotransitive.con".
-inline cic:/CoRN/devel/loeb/per/lst2fun/Fap_tight.con.
+inline "cic:/CoRN/devel/loeb/per/lst2fun/Fap_tight.con".
-inline cic:/CoRN/devel/loeb/per/lst2fun/less.con.
+inline "cic:/CoRN/devel/loeb/per/lst2fun/less.con".
-inline cic:/CoRN/devel/loeb/per/lst2fun/CSetoid_of_less.con.
+inline "cic:/CoRN/devel/loeb/per/lst2fun/CSetoid_of_less.con".