fix

[helm.git] / matita / contribs / CoRN-Decl / algebra / CSetoids.ma

diff --git a/matita/contribs/CoRN-Decl/algebra/CSetoids.ma b/matita/contribs/CoRN-Decl/algebra/CSetoids.ma
index 8d33471fc15afdeb9d67f637da02c7811c5f9194..2f1ed75caf811c3ec5e109eb7d84009e8e07802e 100644 (file)
--- a/matita/contribs/CoRN-Decl/algebra/CSetoids.ma
+++ b/matita/contribs/CoRN-Decl/algebra/CSetoids.ma
@@ -16,6 +16,8 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSetoids".
 
+include "CoRN.ma".
+
 (* $Id.v,v 1.18 2002/11/25 14:43:42 lcf Exp $ *)
 
 (*#* printing [=] %\ensuremath{\equiv}% #≡# *)
@@ -37,15 +39,11 @@ Definition of a constructive setoid with apartness,
 i.e.%\% a set with an equivalence relation and an apartness relation compatible with it.
 *)
 
-(* INCLUDE
-CLogic
-*)
+include "algebra/CLogic.ma".
 
-(* INCLUDE
-Step
-*)
+include "tactics/Step.ma".
 
-inline cic:/CoRN/algebra/CSetoids/Relation.con.
+inline "cic:/CoRN/algebra/CSetoids/Relation.con".
 
 (* End_SpecReals *)
 
@@ -98,15 +96,15 @@ Notice that their type depends on the main logical connective.
 Section Properties_of_relations.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/A.var.
+inline "cic:/CoRN/algebra/CSetoids/A.var".
 
-inline cic:/CoRN/algebra/CSetoids/irreflexive.con.
+inline "cic:/CoRN/algebra/CSetoids/irreflexive.con".
 
-inline cic:/CoRN/algebra/CSetoids/cotransitive.con.
+inline "cic:/CoRN/algebra/CSetoids/cotransitive.con".
 
-inline cic:/CoRN/algebra/CSetoids/tight_apart.con.
+inline "cic:/CoRN/algebra/CSetoids/tight_apart.con".
 
-inline cic:/CoRN/algebra/CSetoids/antisymmetric.con.
+inline "cic:/CoRN/algebra/CSetoids/antisymmetric.con".
 
 (* UNEXPORTED
 End Properties_of_relations.
@@ -129,9 +127,11 @@ Unset Implicit Arguments.
 Apartness, being the main relation, needs to be [CProp]-valued.  Equality,
 as it is characterized by a negative statement, lives in [Prop]. *)
 
-inline cic:/CoRN/algebra/CSetoids/is_CSetoid.ind.
+inline "cic:/CoRN/algebra/CSetoids/is_CSetoid.ind".
 
-inline cic:/CoRN/algebra/CSetoids/CSetoid.ind.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid.ind".
+
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/cs_crr.con 0 (* compounds *).
 
 (* UNEXPORTED
 Implicit Arguments cs_eq [c].
@@ -141,14 +141,26 @@ Implicit Arguments cs_eq [c].
 Implicit Arguments cs_ap [c].
 *)
 
+(* NOTATION
+Infix "[=]" := cs_eq (at level 70, no associativity).
+*)
+
+(* NOTATION
+Infix "[#]" := cs_ap (at level 70, no associativity).
+*)
+
 (* End_SpecReals *)
 
-inline cic:/CoRN/algebra/CSetoids/cs_neq.con.
+inline "cic:/CoRN/algebra/CSetoids/cs_neq.con".
 
 (* UNEXPORTED
 Implicit Arguments cs_neq [S].
 *)
 
+(* NOTATION
+Infix "[~=]" := cs_neq (at level 70, no associativity).
+*)
+
 (*#*
 %\begin{nameconvention}%
 In the names of lemmas, we refer to [ [=] ] by [eq], [ [~=] ] by
@@ -168,17 +180,17 @@ Let [S] be a setoid.
 Section CSetoid_axioms.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/S.var.
+inline "cic:/CoRN/algebra/CSetoids/S.var".
 
-inline cic:/CoRN/algebra/CSetoids/CSetoid_is_CSetoid.con.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid_is_CSetoid.con".
 
-inline cic:/CoRN/algebra/CSetoids/ap_irreflexive.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_irreflexive.con".
 
-inline cic:/CoRN/algebra/CSetoids/ap_symmetric.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_symmetric.con".
 
-inline cic:/CoRN/algebra/CSetoids/ap_cotransitive.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_cotransitive.con".
 
-inline cic:/CoRN/algebra/CSetoids/ap_tight.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_tight.con".
 
 (* UNEXPORTED
 End CSetoid_axioms.
@@ -197,7 +209,7 @@ End CSetoid_axioms.
 Section CSetoid_basics.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/S.var.
+inline "cic:/CoRN/algebra/CSetoids/S.var".
 
 (* End_SpecReals *)
 
@@ -205,13 +217,13 @@ inline cic:/CoRN/algebra/CSetoids/S.var.
 In `there exists a unique [a:S] such that %\ldots%#...#', we now mean unique with respect to the setoid equality. We use [ex_unq] to denote unique existence.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/ex_unq.con.
+inline "cic:/CoRN/algebra/CSetoids/ex_unq.con".
 
-inline cic:/CoRN/algebra/CSetoids/eq_reflexive.con.
+inline "cic:/CoRN/algebra/CSetoids/eq_reflexive.con".
 
-inline cic:/CoRN/algebra/CSetoids/eq_symmetric.con.
+inline "cic:/CoRN/algebra/CSetoids/eq_symmetric.con".
 
-inline cic:/CoRN/algebra/CSetoids/eq_transitive.con.
+inline "cic:/CoRN/algebra/CSetoids/eq_transitive.con".
 
 (*#*
 %\begin{shortcoming}%
@@ -227,23 +239,23 @@ If lemma [a] is just an unfolding of lemma [b], the name of [a] is the name
 %\end{nameconvention}%
 *)
 
-inline cic:/CoRN/algebra/CSetoids/eq_reflexive_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/eq_reflexive_unfolded.con".
 
-inline cic:/CoRN/algebra/CSetoids/eq_symmetric_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/eq_symmetric_unfolded.con".
 
-inline cic:/CoRN/algebra/CSetoids/eq_transitive_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/eq_transitive_unfolded.con".
 
-inline cic:/CoRN/algebra/CSetoids/eq_wdl.con.
+inline "cic:/CoRN/algebra/CSetoids/eq_wdl.con".
 
 (* Begin_SpecReals *)
 
-inline cic:/CoRN/algebra/CSetoids/ap_irreflexive_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_irreflexive_unfolded.con".
 
 (* End_SpecReals *)
 
-inline cic:/CoRN/algebra/CSetoids/ap_cotransitive_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_cotransitive_unfolded.con".
 
-inline cic:/CoRN/algebra/CSetoids/ap_symmetric_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_symmetric_unfolded.con".
 
 (*#*
 %\begin{shortcoming}%
@@ -256,19 +268,19 @@ Therefore we have to split the lemma into the following two lemmas [eq_imp_not_a
 %\end{shortcoming}%
 *)
 
-inline cic:/CoRN/algebra/CSetoids/eq_imp_not_ap.con.
+inline "cic:/CoRN/algebra/CSetoids/eq_imp_not_ap.con".
 
-inline cic:/CoRN/algebra/CSetoids/not_ap_imp_eq.con.
+inline "cic:/CoRN/algebra/CSetoids/not_ap_imp_eq.con".
 
-inline cic:/CoRN/algebra/CSetoids/neq_imp_notnot_ap.con.
+inline "cic:/CoRN/algebra/CSetoids/neq_imp_notnot_ap.con".
 
-inline cic:/CoRN/algebra/CSetoids/notnot_ap_imp_neq.con.
+inline "cic:/CoRN/algebra/CSetoids/notnot_ap_imp_neq.con".
 
-inline cic:/CoRN/algebra/CSetoids/ap_imp_neq.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_imp_neq.con".
 
-inline cic:/CoRN/algebra/CSetoids/not_neq_imp_eq.con.
+inline "cic:/CoRN/algebra/CSetoids/not_neq_imp_eq.con".
 
-inline cic:/CoRN/algebra/CSetoids/eq_imp_not_neq.con.
+inline "cic:/CoRN/algebra/CSetoids/eq_imp_not_neq.con".
 
 (* Begin_SpecReals *)
 
@@ -284,13 +296,13 @@ Section product_csetoid.
 
 (*#* **The product of setoids *)
 
-inline cic:/CoRN/algebra/CSetoids/prod_ap.con.
+inline "cic:/CoRN/algebra/CSetoids/prod_ap.con".
 
-inline cic:/CoRN/algebra/CSetoids/prod_eq.con.
+inline "cic:/CoRN/algebra/CSetoids/prod_eq.con".
 
-inline cic:/CoRN/algebra/CSetoids/prodcsetoid_is_CSetoid.con.
+inline "cic:/CoRN/algebra/CSetoids/prodcsetoid_is_CSetoid.con".
 
-inline cic:/CoRN/algebra/CSetoids/ProdCSetoid.con.
+inline "cic:/CoRN/algebra/CSetoids/ProdCSetoid.con".
 
 (* UNEXPORTED
 End product_csetoid.
@@ -336,7 +348,7 @@ on predicates and relations.
 Section CSetoid_relations_and_predicates.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/S.var.
+inline "cic:/CoRN/algebra/CSetoids/S.var".
 
 (* End_SpecReals *)
 
@@ -352,19 +364,21 @@ At this stage, we consider [CProp]- and [Prop]-valued predicates on setoids.
 Section CSetoidPredicates.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/P.var.
+inline "cic:/CoRN/algebra/CSetoids/P.var".
 
-inline cic:/CoRN/algebra/CSetoids/pred_strong_ext.con.
+inline "cic:/CoRN/algebra/CSetoids/pred_strong_ext.con".
 
-inline cic:/CoRN/algebra/CSetoids/pred_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/pred_wd.con".
 
 (* UNEXPORTED
 End CSetoidPredicates.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/CSetoid_predicate.ind.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid_predicate.ind".
 
-inline cic:/CoRN/algebra/CSetoids/csp_wd.con.
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/csp_pred.con 0 (* compounds *).
+
+inline "cic:/CoRN/algebra/CSetoids/csp_wd.con".
 
 (*#* Similar, with [Prop] instead of [CProp]. *)
 
@@ -372,11 +386,11 @@ inline cic:/CoRN/algebra/CSetoids/csp_wd.con.
 Section CSetoidPPredicates.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/P.var.
+inline "cic:/CoRN/algebra/CSetoids/P.var".
 
-inline cic:/CoRN/algebra/CSetoids/pred_strong_ext'.con.
+inline "cic:/CoRN/algebra/CSetoids/pred_strong_ext'.con".
 
-inline cic:/CoRN/algebra/CSetoids/pred_wd'.con.
+inline "cic:/CoRN/algebra/CSetoids/pred_wd'.con".
 
 (* UNEXPORTED
 End CSetoidPPredicates.
@@ -384,9 +398,11 @@ End CSetoidPPredicates.
 
 (*#* ***Definition of a setoid predicate *)
 
-inline cic:/CoRN/algebra/CSetoids/CSetoid_predicate'.ind.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid_predicate'.ind".
+
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/csp'_pred.con 0 (* compounds *).
 
-inline cic:/CoRN/algebra/CSetoids/csp'_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/csp'_wd.con".
 
 (* Begin_SpecReals *)
 
@@ -399,25 +415,25 @@ Let [R] be a relation on (the carrier of) [S].
 Section CsetoidRelations.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/R.var.
+inline "cic:/CoRN/algebra/CSetoids/R.var".
 
-inline cic:/CoRN/algebra/CSetoids/rel_wdr.con.
+inline "cic:/CoRN/algebra/CSetoids/rel_wdr.con".
 
-inline cic:/CoRN/algebra/CSetoids/rel_wdl.con.
+inline "cic:/CoRN/algebra/CSetoids/rel_wdl.con".
 
-inline cic:/CoRN/algebra/CSetoids/rel_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/rel_strext.con".
 
 (* End_SpecReals *)
 
-inline cic:/CoRN/algebra/CSetoids/rel_strext_lft.con.
+inline "cic:/CoRN/algebra/CSetoids/rel_strext_lft.con".
 
-inline cic:/CoRN/algebra/CSetoids/rel_strext_rht.con.
+inline "cic:/CoRN/algebra/CSetoids/rel_strext_rht.con".
 
-inline cic:/CoRN/algebra/CSetoids/rel_strext_imp_lftarg.con.
+inline "cic:/CoRN/algebra/CSetoids/rel_strext_imp_lftarg.con".
 
-inline cic:/CoRN/algebra/CSetoids/rel_strext_imp_rhtarg.con.
+inline "cic:/CoRN/algebra/CSetoids/rel_strext_imp_rhtarg.con".
 
-inline cic:/CoRN/algebra/CSetoids/rel_strextarg_imp_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/rel_strextarg_imp_strext.con".
 
 (* Begin_SpecReals *)
 
@@ -428,7 +444,9 @@ End CsetoidRelations.
 (*#* ***Definition of a setoid relation
 The type of relations over a setoid.  *)
 
-inline cic:/CoRN/algebra/CSetoids/CSetoid_relation.ind.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid_relation.ind".
+
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/csr_rel.con 0 (* compounds *).
 
 (*#* ***[CProp] Relations
 %\begin{convention}%
@@ -440,25 +458,25 @@ Let [R] be a relation on (the carrier of) [S].
 Section CCsetoidRelations.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/R.var.
+inline "cic:/CoRN/algebra/CSetoids/R.var".
 
-inline cic:/CoRN/algebra/CSetoids/Crel_wdr.con.
+inline "cic:/CoRN/algebra/CSetoids/Crel_wdr.con".
 
-inline cic:/CoRN/algebra/CSetoids/Crel_wdl.con.
+inline "cic:/CoRN/algebra/CSetoids/Crel_wdl.con".
 
-inline cic:/CoRN/algebra/CSetoids/Crel_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/Crel_strext.con".
 
 (* End_SpecReals *)
 
-inline cic:/CoRN/algebra/CSetoids/Crel_strext_lft.con.
+inline "cic:/CoRN/algebra/CSetoids/Crel_strext_lft.con".
 
-inline cic:/CoRN/algebra/CSetoids/Crel_strext_rht.con.
+inline "cic:/CoRN/algebra/CSetoids/Crel_strext_rht.con".
 
-inline cic:/CoRN/algebra/CSetoids/Crel_strext_imp_lftarg.con.
+inline "cic:/CoRN/algebra/CSetoids/Crel_strext_imp_lftarg.con".
 
-inline cic:/CoRN/algebra/CSetoids/Crel_strext_imp_rhtarg.con.
+inline "cic:/CoRN/algebra/CSetoids/Crel_strext_imp_rhtarg.con".
 
-inline cic:/CoRN/algebra/CSetoids/Crel_strextarg_imp_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/Crel_strextarg_imp_strext.con".
 
 (* Begin_SpecReals *)
 
@@ -470,25 +488,27 @@ End CCsetoidRelations.
 
 The type of relations over a setoid.  *)
 
-inline cic:/CoRN/algebra/CSetoids/CCSetoid_relation.ind.
+inline "cic:/CoRN/algebra/CSetoids/CCSetoid_relation.ind".
 
-inline cic:/CoRN/algebra/CSetoids/Ccsr_wdr.con.
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/Ccsr_rel.con 0 (* compounds *).
 
-inline cic:/CoRN/algebra/CSetoids/Ccsr_wdl.con.
+inline "cic:/CoRN/algebra/CSetoids/Ccsr_wdr.con".
+
+inline "cic:/CoRN/algebra/CSetoids/Ccsr_wdl.con".
 
 (* End_SpecReals *)
 
-inline cic:/CoRN/algebra/CSetoids/ap_wdr.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_wdr.con".
 
-inline cic:/CoRN/algebra/CSetoids/ap_wdl.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_wdl.con".
 
-inline cic:/CoRN/algebra/CSetoids/ap_wdr_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_wdr_unfolded.con".
 
-inline cic:/CoRN/algebra/CSetoids/ap_wdl_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_wdl_unfolded.con".
 
-inline cic:/CoRN/algebra/CSetoids/ap_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/ap_strext.con".
 
-inline cic:/CoRN/algebra/CSetoids/predS_well_def.con.
+inline "cic:/CoRN/algebra/CSetoids/predS_well_def.con".
 
 (* Begin_SpecReals *)
 
@@ -523,11 +543,11 @@ First we consider unary functions.  *)
 Section CSetoid_functions.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/S1.var.
+inline "cic:/CoRN/algebra/CSetoids/S1.var".
 
-inline cic:/CoRN/algebra/CSetoids/S2.var.
+inline "cic:/CoRN/algebra/CSetoids/S2.var".
 
-inline cic:/CoRN/algebra/CSetoids/S3.var.
+inline "cic:/CoRN/algebra/CSetoids/S3.var".
 
 (* UNEXPORTED
 Section unary_functions.
@@ -538,15 +558,15 @@ In the following two definitions,
 [f] is a function from (the carrier of) [S1] to
 (the carrier of) [S2].  *)
 
-inline cic:/CoRN/algebra/CSetoids/f.var.
+inline "cic:/CoRN/algebra/CSetoids/f.var".
 
-inline cic:/CoRN/algebra/CSetoids/fun_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/fun_wd.con".
 
-inline cic:/CoRN/algebra/CSetoids/fun_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/fun_strext.con".
 
 (* End_SpecReals *)
 
-inline cic:/CoRN/algebra/CSetoids/fun_strext_imp_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/fun_strext_imp_wd.con".
 
 (* Begin_SpecReals *)
 
@@ -554,13 +574,15 @@ inline cic:/CoRN/algebra/CSetoids/fun_strext_imp_wd.con.
 End unary_functions.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/CSetoid_fun.ind.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid_fun.ind".
+
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/csf_fun.con 0 (* compounds *).
 
-inline cic:/CoRN/algebra/CSetoids/csf_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/csf_wd.con".
 
 (* End_SpecReals *)
 
-inline cic:/CoRN/algebra/CSetoids/Const_CSetoid_fun.con.
+inline "cic:/CoRN/algebra/CSetoids/Const_CSetoid_fun.con".
 
 (* Begin_SpecReals *)
 
@@ -574,15 +596,15 @@ In the following two definitions,
 [f] is a function from [S1] and [S2] to [S3].
 *)
 
-inline cic:/CoRN/algebra/CSetoids/f.var.
+inline "cic:/CoRN/algebra/CSetoids/f.var".
 
-inline cic:/CoRN/algebra/CSetoids/bin_fun_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_fun_wd.con".
 
-inline cic:/CoRN/algebra/CSetoids/bin_fun_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_fun_strext.con".
 
 (* End_SpecReals *)
 
-inline cic:/CoRN/algebra/CSetoids/bin_fun_strext_imp_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_fun_strext_imp_wd.con".
 
 (* Begin_SpecReals *)
 
@@ -590,15 +612,17 @@ inline cic:/CoRN/algebra/CSetoids/bin_fun_strext_imp_wd.con.
 End binary_functions.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/CSetoid_bin_fun.ind.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid_bin_fun.ind".
 
-inline cic:/CoRN/algebra/CSetoids/csbf_wd.con.
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/csbf_fun.con 0 (* compounds *).
 
-inline cic:/CoRN/algebra/CSetoids/csf_wd_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/csbf_wd.con".
 
-inline cic:/CoRN/algebra/CSetoids/csf_strext_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/csf_wd_unfolded.con".
 
-inline cic:/CoRN/algebra/CSetoids/csbf_wd_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/csf_strext_unfolded.con".
+
+inline "cic:/CoRN/algebra/CSetoids/csbf_wd_unfolded.con".
 
 (* UNEXPORTED
 End CSetoid_functions.
@@ -637,87 +661,91 @@ Let [S] be a setoid.
 Section csetoid_inner_ops.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/S.var.
+inline "cic:/CoRN/algebra/CSetoids/S.var".
 
 (*#* Properties of binary operations *)
 
-inline cic:/CoRN/algebra/CSetoids/commutes.con.
+inline "cic:/CoRN/algebra/CSetoids/commutes.con".
 
-inline cic:/CoRN/algebra/CSetoids/associative.con.
+inline "cic:/CoRN/algebra/CSetoids/associative.con".
 
 (*#* Well-defined unary operations on a setoid.  *)
 
-inline cic:/CoRN/algebra/CSetoids/un_op_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/un_op_wd.con".
 
-inline cic:/CoRN/algebra/CSetoids/un_op_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/un_op_strext.con".
 
-inline cic:/CoRN/algebra/CSetoids/CSetoid_un_op.con.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid_un_op.con".
 
-inline cic:/CoRN/algebra/CSetoids/Build_CSetoid_un_op.con.
+inline "cic:/CoRN/algebra/CSetoids/Build_CSetoid_un_op.con".
 
 (* End_SpecReals *)
 
-inline cic:/CoRN/algebra/CSetoids/id_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/id_strext.con".
 
-inline cic:/CoRN/algebra/CSetoids/id_pres_eq.con.
+inline "cic:/CoRN/algebra/CSetoids/id_pres_eq.con".
 
-inline cic:/CoRN/algebra/CSetoids/id_un_op.con.
+inline "cic:/CoRN/algebra/CSetoids/id_un_op.con".
 
 (* begin hide *)
 
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/un_op_fun.con 0 (* compounds *).
+
 (* end hide *)
 
 (* Begin_SpecReals *)
 
-inline cic:/CoRN/algebra/CSetoids/cs_un_op_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/cs_un_op_strext.con".
 
 (* End_SpecReals *)
 
-inline cic:/CoRN/algebra/CSetoids/un_op_wd_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/un_op_wd_unfolded.con".
 
-inline cic:/CoRN/algebra/CSetoids/un_op_strext_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/un_op_strext_unfolded.con".
 
 (*#* Well-defined binary operations on a setoid.  *)
 
-inline cic:/CoRN/algebra/CSetoids/bin_op_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op_wd.con".
 
-inline cic:/CoRN/algebra/CSetoids/bin_op_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op_strext.con".
 
 (* Begin_SpecReals *)
 
-inline cic:/CoRN/algebra/CSetoids/CSetoid_bin_op.con.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid_bin_op.con".
 
-inline cic:/CoRN/algebra/CSetoids/Build_CSetoid_bin_op.con.
+inline "cic:/CoRN/algebra/CSetoids/Build_CSetoid_bin_op.con".
 
 (* End_SpecReals *)
 
-inline cic:/CoRN/algebra/CSetoids/cs_bin_op_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/cs_bin_op_wd.con".
 
-inline cic:/CoRN/algebra/CSetoids/cs_bin_op_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/cs_bin_op_strext.con".
 
 (* Begin_SpecReals *)
 
 (* begin hide *)
 
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/bin_op_bin_fun.con 0 (* compounds *).
+
 (* end hide *)
 
 (* End_SpecReals *)
 
-inline cic:/CoRN/algebra/CSetoids/bin_op_wd_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op_wd_unfolded.con".
 
-inline cic:/CoRN/algebra/CSetoids/bin_op_strext_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op_strext_unfolded.con".
 
-inline cic:/CoRN/algebra/CSetoids/bin_op_is_wd_un_op_lft.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op_is_wd_un_op_lft.con".
 
-inline cic:/CoRN/algebra/CSetoids/bin_op_is_wd_un_op_rht.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op_is_wd_un_op_rht.con".
 
-inline cic:/CoRN/algebra/CSetoids/bin_op_is_strext_un_op_lft.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op_is_strext_un_op_lft.con".
 
-inline cic:/CoRN/algebra/CSetoids/bin_op_is_strext_un_op_rht.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op_is_strext_un_op_rht.con".
 
-inline cic:/CoRN/algebra/CSetoids/bin_op2un_op_rht.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op2un_op_rht.con".
 
-inline cic:/CoRN/algebra/CSetoids/bin_op2un_op_lft.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op2un_op_lft.con".
 
 (* Begin_SpecReals *)
 
@@ -753,31 +781,33 @@ Let [S1] and [S2] be setoids.
 Section csetoid_outer_ops.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/S1.var.
+inline "cic:/CoRN/algebra/CSetoids/S1.var".
 
-inline cic:/CoRN/algebra/CSetoids/S2.var.
+inline "cic:/CoRN/algebra/CSetoids/S2.var".
 
 (*#*
 Well-defined outer operations on a setoid.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/outer_op_well_def.con.
+inline "cic:/CoRN/algebra/CSetoids/outer_op_well_def.con".
 
-inline cic:/CoRN/algebra/CSetoids/outer_op_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/outer_op_strext.con".
 
-inline cic:/CoRN/algebra/CSetoids/CSetoid_outer_op.con.
+inline "cic:/CoRN/algebra/CSetoids/CSetoid_outer_op.con".
 
-inline cic:/CoRN/algebra/CSetoids/Build_CSetoid_outer_op.con.
+inline "cic:/CoRN/algebra/CSetoids/Build_CSetoid_outer_op.con".
 
-inline cic:/CoRN/algebra/CSetoids/csoo_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/csoo_wd.con".
 
-inline cic:/CoRN/algebra/CSetoids/csoo_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/csoo_strext.con".
 
 (* begin hide *)
 
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/outer_op_bin_fun.con 0 (* compounds *).
+
 (* end hide *)
 
-inline cic:/CoRN/algebra/CSetoids/csoo_wd_unfolded.con.
+inline "cic:/CoRN/algebra/CSetoids/csoo_wd_unfolded.con".
 
 (* UNEXPORTED
 End csetoid_outer_ops.
@@ -799,34 +829,36 @@ Let [S] be a setoid, and [P] a predicate on the carrier of [S].
 Section SubCSetoids.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/S.var.
+inline "cic:/CoRN/algebra/CSetoids/S.var".
+
+inline "cic:/CoRN/algebra/CSetoids/P.var".
 
-inline cic:/CoRN/algebra/CSetoids/P.var.
+inline "cic:/CoRN/algebra/CSetoids/subcsetoid_crr.ind".
 
-inline cic:/CoRN/algebra/CSetoids/subcsetoid_crr.ind.
+coercion cic:/matita/CoRN-Decl/algebra/CSetoids/scs_elem.con 0 (* compounds *).
 
 (*#* Though [scs_elem] is declared as a coercion, it does not satisfy the
 uniform inheritance condition and will not be inserted.  However it will
 also not be printed, which is handy.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/restrict_relation.con.
+inline "cic:/CoRN/algebra/CSetoids/restrict_relation.con".
 
-inline cic:/CoRN/algebra/CSetoids/Crestrict_relation.con.
+inline "cic:/CoRN/algebra/CSetoids/Crestrict_relation.con".
 
-inline cic:/CoRN/algebra/CSetoids/subcsetoid_eq.con.
+inline "cic:/CoRN/algebra/CSetoids/subcsetoid_eq.con".
 
-inline cic:/CoRN/algebra/CSetoids/subcsetoid_ap.con.
+inline "cic:/CoRN/algebra/CSetoids/subcsetoid_ap.con".
 
 (* End_SpecReals *)
 
-inline cic:/CoRN/algebra/CSetoids/subcsetoid_equiv.con.
+inline "cic:/CoRN/algebra/CSetoids/subcsetoid_equiv.con".
 
 (* Begin_SpecReals *)
 
-inline cic:/CoRN/algebra/CSetoids/subcsetoid_is_CSetoid.con.
+inline "cic:/CoRN/algebra/CSetoids/subcsetoid_is_CSetoid.con".
 
-inline cic:/CoRN/algebra/CSetoids/Build_SubCSetoid.con.
+inline "cic:/CoRN/algebra/CSetoids/Build_SubCSetoid.con".
 
 (* End_SpecReals *)
 
@@ -840,24 +872,24 @@ Let [f] be a unary setoid operation on [S].
 Section SubCSetoid_unary_operations.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/f.var.
+inline "cic:/CoRN/algebra/CSetoids/f.var".
 
-inline cic:/CoRN/algebra/CSetoids/un_op_pres_pred.con.
+inline "cic:/CoRN/algebra/CSetoids/un_op_pres_pred.con".
 
 (*#*
 %\begin{convention}%
 Assume [pr:un_op_pres_pred].
 %\end{convention}% *)
 
-inline cic:/CoRN/algebra/CSetoids/pr.var.
+inline "cic:/CoRN/algebra/CSetoids/pr.var".
 
-inline cic:/CoRN/algebra/CSetoids/restr_un_op.con.
+inline "cic:/CoRN/algebra/CSetoids/restr_un_op.con".
 
-inline cic:/CoRN/algebra/CSetoids/restr_un_op_wd.con.
+inline "cic:/CoRN/algebra/CSetoids/restr_un_op_wd.con".
 
-inline cic:/CoRN/algebra/CSetoids/restr_un_op_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/restr_un_op_strext.con".
 
-inline cic:/CoRN/algebra/CSetoids/Build_SubCSetoid_un_op.con.
+inline "cic:/CoRN/algebra/CSetoids/Build_SubCSetoid_un_op.con".
 
 (* UNEXPORTED
 End SubCSetoid_unary_operations.
@@ -873,9 +905,9 @@ Let [f] be a binary setoid operation on [S].
 Section SubCSetoid_binary_operations.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/f.var.
+inline "cic:/CoRN/algebra/CSetoids/f.var".
 
-inline cic:/CoRN/algebra/CSetoids/bin_op_pres_pred.con.
+inline "cic:/CoRN/algebra/CSetoids/bin_op_pres_pred.con".
 
 (*#*
 %\begin{convention}%
@@ -883,17 +915,17 @@ Assume [bin_op_pres_pred].
 %\end{convention}%
 *)
 
-inline cic:/CoRN/algebra/CSetoids/pr.var.
+inline "cic:/CoRN/algebra/CSetoids/pr.var".
 
-inline cic:/CoRN/algebra/CSetoids/restr_bin_op.con.
+inline "cic:/CoRN/algebra/CSetoids/restr_bin_op.con".
 
-inline cic:/CoRN/algebra/CSetoids/restr_bin_op_well_def.con.
+inline "cic:/CoRN/algebra/CSetoids/restr_bin_op_well_def.con".
 
-inline cic:/CoRN/algebra/CSetoids/restr_bin_op_strext.con.
+inline "cic:/CoRN/algebra/CSetoids/restr_bin_op_strext.con".
 
-inline cic:/CoRN/algebra/CSetoids/Build_SubCSetoid_bin_op.con.
+inline "cic:/CoRN/algebra/CSetoids/Build_SubCSetoid_bin_op.con".
 
-inline cic:/CoRN/algebra/CSetoids/restr_f_assoc.con.
+inline "cic:/CoRN/algebra/CSetoids/restr_f_assoc.con".
 
 (* UNEXPORTED
 End SubCSetoid_binary_operations.
@@ -922,15 +954,15 @@ Tactic Notation "Step_final" constr(c) :=  Step_final c.
 (*#* **Miscellaneous
 *)
 
-inline cic:/CoRN/algebra/CSetoids/proper_caseZ_diff_CS.con.
+inline "cic:/CoRN/algebra/CSetoids/proper_caseZ_diff_CS.con".
 
 (*#*
 Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates.
 *)
 
-inline cic:/CoRN/algebra/CSetoids/nat_less_n_fun.con.
+inline "cic:/CoRN/algebra/CSetoids/nat_less_n_fun.con".
 
-inline cic:/CoRN/algebra/CSetoids/nat_less_n_fun'.con.
+inline "cic:/CoRN/algebra/CSetoids/nat_less_n_fun'.con".
 
 (* UNEXPORTED
 Implicit Arguments nat_less_n_fun [S n].