From: Enrico Tassi Date: Mon, 7 Apr 2008 16:19:11 +0000 (+0000) Subject: commented out uris of objs that do not compile properly X-Git-Tag: make_still_working~5418 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3c7db631a1cbb1d91f3109431c046ef78c3d89b9;p=helm.git commented out uris of objs that do not compile properly --- diff --git a/helm/software/components/ng_kernel/alluris.txt b/helm/software/components/ng_kernel/alluris.txt index 01add230a..84385385c 100644 --- a/helm/software/components/ng_kernel/alluris.txt +++ b/helm/software/components/ng_kernel/alluris.txt @@ -1,3 +1,23 @@ +cic:/matita/demo/realisability/type_OF_SP.con +cic:/matita/demo/realisability/true_impl_realized.con +cic:/matita/demo/realisability/sigma_rect.con +cic:/matita/demo/realisability/sigma_rec.con +cic:/matita/demo/realisability/sigma_ind.con +cic:/matita/demo/realisability/sigma.ind +cic:/matita/demo/realisability/realized.con +cic:/matita/demo/realisability/pi2.con +cic:/matita/demo/realisability/pi1.con +cic:/matita/demo/realisability/modr.con +cic:/matita/demo/realisability/id_axiom.con +cic:/matita/demo/realisability/extraction.con +cic:/matita/demo/realisability/elim_abs.con +cic:/matita/demo/realisability/cut.con +cic:/matita/demo/realisability/and_i.con +cic:/matita/demo/realisability/SP_rect.con +cic:/matita/demo/realisability/SP_rec.con +cic:/matita/demo/realisability/SP_ind.con +cic:/matita/demo/realisability/SP.ind +cic:/matita/demo/realisability/Prop_OF_SP.con cic:/matita/Q/Qaxioms/symmetric_Qtimes.con cic:/matita/Q/Qaxioms/symmetric_Qplus.con cic:/matita/Q/Qaxioms/sigma_Q.con @@ -1548,8 +1568,6 @@ cic:/matita/algebra/CoRN/SemiGroups/CSemiGroup_rec.con cic:/matita/algebra/CoRN/SemiGroups/CSemiGroup_is_CSemiGroup.con cic:/matita/algebra/CoRN/SemiGroups/CSemiGroup_ind.con cic:/matita/algebra/CoRN/SemiGroups/CSemiGroup.ind -cic:/matita/algebra/CoRN/SemiGroups/Astar_is_CSemiGroup.con -cic:/matita/algebra/CoRN/SemiGroups/Astar_as_CSemiGroup.con cic:/matita/algebra/CoRN/SetoidFun/total_eq_part.con cic:/matita/algebra/CoRN/SetoidFun/ta_apfun.con cic:/matita/algebra/CoRN/SetoidFun/sym_apfun.con @@ -1588,8 +1606,6 @@ cic:/matita/algebra/CoRN/SetoidFun/injective.con cic:/matita/algebra/CoRN/SetoidFun/inj2.con cic:/matita/algebra/CoRN/SetoidFun/inj1.con cic:/matita/algebra/CoRN/SetoidFun/id_is_bij.con -cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_is_CSetoid.con -cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_as_csetoid.con cic:/matita/algebra/CoRN/SetoidFun/extension_wd.con cic:/matita/algebra/CoRN/SetoidFun/extend.con cic:/matita/algebra/CoRN/SetoidFun/ext2_a.con @@ -1626,56 +1642,6 @@ cic:/matita/algebra/CoRN/SetoidFun/bin_part_function_comp_dom_wd.con cic:/matita/algebra/CoRN/SetoidFun/bijective.con cic:/matita/algebra/CoRN/SetoidFun/bdom_wd.con cic:/matita/algebra/CoRN/SetoidFun/assoc_comp.con -cic:/matita/algebra/CoRN/SetoidFun/app_strext.con -cic:/matita/algebra/CoRN/SetoidFun/app_as_csb_fun.con -cic:/matita/algebra/CoRN/SetoidFun/appA.con -cic:/matita/algebra/CoRN/SetoidFun/ap_fun.con -cic:/matita/algebra/CoRN/SetoidFun/ap_fm_tight.con -cic:/matita/algebra/CoRN/SetoidFun/ap_fm_symmetric.con -cic:/matita/algebra/CoRN/SetoidFun/ap_fm_irreflexive.con -cic:/matita/algebra/CoRN/SetoidFun/ap_fm_cotransitive.con -cic:/matita/algebra/CoRN/SetoidFun/UR.con -cic:/matita/algebra/CoRN/SetoidFun/UQ.con -cic:/matita/algebra/CoRN/SetoidFun/UP.con -cic:/matita/algebra/CoRN/SetoidFun/Tlist_rect.con -cic:/matita/algebra/CoRN/SetoidFun/Tlist_rec.con -cic:/matita/algebra/CoRN/SetoidFun/Tlist_ind.con -cic:/matita/algebra/CoRN/SetoidFun/Tlist.ind -cic:/matita/algebra/CoRN/SetoidFun/Tapp.con -cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom1.con -cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom.con -cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom1.con -cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom.con -cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rect.con -cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rec.con -cic:/matita/algebra/CoRN/SetoidFun/PartFunct_ind.con -cic:/matita/algebra/CoRN/SetoidFun/PartFunct.ind -cic:/matita/algebra/CoRN/SetoidFun/Inv_bij.con -cic:/matita/algebra/CoRN/SetoidFun/Inv.con -cic:/matita/algebra/CoRN/SetoidFun/Fid.con -cic:/matita/algebra/CoRN/SetoidFun/Fconst.con -cic:/matita/algebra/CoRN/SetoidFun/Fcomp.con -cic:/matita/algebra/CoRN/SetoidFun/FS_is_CSetoid.con -cic:/matita/algebra/CoRN/SetoidFun/FS_as_CSetoid.con -cic:/matita/algebra/CoRN/SetoidFun/Dir_bij.con -cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rect.con -cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rec.con -cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_ind.con -cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun.ind -cic:/matita/algebra/CoRN/SetoidFun/CSap_fm.con -cic:/matita/algebra/CoRN/SetoidFun/CAnd_rect.con -cic:/matita/algebra/CoRN/SetoidFun/CAnd_rec.con -cic:/matita/algebra/CoRN/SetoidFun/CAnd_ind.con -cic:/matita/algebra/CoRN/SetoidFun/CAnd.ind -cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rect.con -cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rec.con -cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_ind.con -cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct.ind -cic:/matita/algebra/CoRN/SetoidFun/BinFcomp.con -cic:/matita/algebra/CoRN/SetoidFun/BR.con -cic:/matita/algebra/CoRN/SetoidFun/BQ.con -cic:/matita/algebra/CoRN/SetoidFun/BP.con -cic:/matita/algebra/CoRN/SetoidFun/Astar.con cic:/matita/algebra/CoRN/SetoidInc/included_trans.con cic:/matita/algebra/CoRN/SetoidInc/included_refl.con cic:/matita/algebra/CoRN/SetoidInc/included_extend.con @@ -2064,7 +2030,6 @@ cic:/matita/demo/propositional_sequent_calculus/or_of_list_permut.con cic:/matita/demo/propositional_sequent_calculus/or_of_list.con cic:/matita/demo/propositional_sequent_calculus/not_nf_inv.con cic:/matita/demo/propositional_sequent_calculus/not_nf_ind.con -cic:/matita/demo/propositional_sequent_calculus/not_nf_elim_not.con cic:/matita/demo/propositional_sequent_calculus/not_nf.ind cic:/matita/demo/propositional_sequent_calculus/not_eq_nil_append_cons.con cic:/matita/demo/propositional_sequent_calculus/negate.con @@ -2078,47 +2043,6 @@ cic:/matita/demo/propositional_sequent_calculus/eval.con cic:/matita/demo/propositional_sequent_calculus/eq_to_eq_mem.con cic:/matita/demo/propositional_sequent_calculus/eq_plus_n_m_O_to_eq_m_O.con cic:/matita/demo/propositional_sequent_calculus/eq_notb_notb_b_b.con -cic:/matita/demo/propositional_sequent_calculus/eq_eval_elim_not_eval.con -cic:/matita/demo/propositional_sequent_calculus/elim_not.con -cic:/matita/demo/propositional_sequent_calculus/distributive_orb_andb.con -cic:/matita/demo/propositional_sequent_calculus/distributive_andb_orb.con -cic:/matita/demo/propositional_sequent_calculus/derive_inv.con -cic:/matita/demo/propositional_sequent_calculus/derive_ind.con -cic:/matita/demo/propositional_sequent_calculus/derive.ind -cic:/matita/demo/propositional_sequent_calculus/demorgan2.con -cic:/matita/demo/propositional_sequent_calculus/demorgan1.con -cic:/matita/demo/propositional_sequent_calculus/daemon.con -cic:/matita/demo/propositional_sequent_calculus/completeness_base.con -cic:/matita/demo/propositional_sequent_calculus/associative_andb.con -cic:/matita/demo/propositional_sequent_calculus/assoc_orb.con -cic:/matita/demo/propositional_sequent_calculus/and_of_list_permut.con -cic:/matita/demo/propositional_sequent_calculus/and_of_list.con -cic:/matita/demo/propositional_sequent_calculus/Formula_rect.con -cic:/matita/demo/propositional_sequent_calculus/Formula_rec.con -cic:/matita/demo/propositional_sequent_calculus/Formula_ind.con -cic:/matita/demo/propositional_sequent_calculus/Formula.ind -cic:/matita/demo/realisability/type_OF_SP.con -cic:/matita/demo/realisability/true_impl_realized.con -cic:/matita/demo/realisability/sigma_rect.con -cic:/matita/demo/realisability/sigma_rec.con -cic:/matita/demo/realisability/sigma_ind.con -cic:/matita/demo/realisability/sigma.ind -cic:/matita/demo/realisability/realized.con -cic:/matita/demo/realisability/pi2.con -cic:/matita/demo/realisability/pi1.con -cic:/matita/demo/realisability/modr.con -cic:/matita/demo/realisability/id_axiom.con -cic:/matita/demo/realisability/extraction.con -cic:/matita/demo/realisability/elim_abs.con -cic:/matita/demo/realisability/cut.con -cic:/matita/demo/realisability/correct2.con -cic:/matita/demo/realisability/correct.con -cic:/matita/demo/realisability/and_i.con -cic:/matita/demo/realisability/SP_rect.con -cic:/matita/demo/realisability/SP_rec.con -cic:/matita/demo/realisability/SP_ind.con -cic:/matita/demo/realisability/SP.ind -cic:/matita/demo/realisability/Prop_OF_SP.con cic:/matita/technicalities/setoids/variance_rect.con cic:/matita/technicalities/setoids/variance_rec.con cic:/matita/technicalities/setoids/variance_of_argument_class.con @@ -2129,77 +2053,159 @@ cic:/matita/technicalities/setoids/rewrite_direction_rec.con cic:/matita/technicalities/setoids/rewrite_direction_ind.con cic:/matita/technicalities/setoids/rewrite_direction.ind cic:/matita/technicalities/setoids/relation_of_relation_class.con -cic:/matita/technicalities/setoids/relation_of_product_of_arguments.con cic:/matita/technicalities/setoids/relation_of_areflexive_relation_class.con cic:/matita/technicalities/setoids/relation_class_of_reflexive_relation_class.con cic:/matita/technicalities/setoids/relation_class_of_argument_class.con cic:/matita/technicalities/setoids/relation_class_of_areflexive_relation_class.con -cic:/matita/technicalities/setoids/product_of_arguments.con -cic:/matita/technicalities/setoids/opposite_direction_idempotent.con -cic:/matita/technicalities/setoids/opposite_direction.con -cic:/matita/technicalities/setoids/nelistT_rect.con -cic:/matita/technicalities/setoids/nelistT_rec.con -cic:/matita/technicalities/setoids/nelistT_ind.con -cic:/matita/technicalities/setoids/nelistT.ind -cic:/matita/technicalities/setoids/morphism_theory_of_predicate.con -cic:/matita/technicalities/setoids/morphism_theory_of_function.con -cic:/matita/technicalities/setoids/make_compatibility_goal_aux.con -cic:/matita/technicalities/setoids/make_compatibility_goal.con -cic:/matita/technicalities/setoids/list_of_Leibniz_of_list_of_types.con -cic:/matita/technicalities/setoids/interp_relation_class_list.con -cic:/matita/technicalities/setoids/interp.con -cic:/matita/technicalities/setoids/impl_trans.con -cic:/matita/technicalities/setoids/impl_refl.con -cic:/matita/technicalities/setoids/impl.con -cic:/matita/technicalities/setoids/get_rewrite_direction.con -cic:/matita/technicalities/setoids/function_type_of_morphism_signature.con -cic:/matita/technicalities/setoids/equality_morphism_of_symmetric_reflexive_transitive_relation.con -cic:/matita/technicalities/setoids/equality_morphism_of_symmetric_areflexive_transitive_relation.con -cic:/matita/technicalities/setoids/equality_morphism_of_asymmetric_reflexive_transitive_relation.con -cic:/matita/technicalities/setoids/equality_morphism_of_asymmetric_areflexive_transitive_relation.con -cic:/matita/technicalities/setoids/directed_relation_of_relation_class.con -cic:/matita/technicalities/setoids/directed_relation_of_argument_class.con -cic:/matita/technicalities/setoids/check_if_variance_is_respected_inv.con -cic:/matita/technicalities/setoids/check_if_variance_is_respected_ind.con -cic:/matita/technicalities/setoids/check_if_variance_is_respected.ind -cic:/matita/technicalities/setoids/carrier_of_relation_class.con -cic:/matita/technicalities/setoids/carrier_of_reflexive_relation_class.con -cic:/matita/technicalities/setoids/carrier_of_areflexive_relation_class.con -cic:/matita/technicalities/setoids/apply_morphism_compatibility_Right2Left.con -cic:/matita/technicalities/setoids/apply_morphism_compatibility_Left2Right.con -cic:/matita/technicalities/setoids/apply_morphism.con -cic:/matita/technicalities/setoids/about_carrier_of_relation_class_and_relation_class_of_argument_class.con -cic:/matita/technicalities/setoids/X_Relation_Class_rect.con -cic:/matita/technicalities/setoids/X_Relation_Class_rec.con -cic:/matita/technicalities/setoids/X_Relation_Class_ind.con -cic:/matita/technicalities/setoids/X_Relation_Class.ind -cic:/matita/technicalities/setoids/Relation_Class.con -cic:/matita/technicalities/setoids/Reflexive_Relation_Class_rect.con -cic:/matita/technicalities/setoids/Reflexive_Relation_Class_rec.con -cic:/matita/technicalities/setoids/Reflexive_Relation_Class_ind.con -cic:/matita/technicalities/setoids/Reflexive_Relation_Class.ind -cic:/matita/technicalities/setoids/Morphism_Theory_rect.con -cic:/matita/technicalities/setoids/Morphism_Theory_rec.con -cic:/matita/technicalities/setoids/Morphism_Theory_ind.con -cic:/matita/technicalities/setoids/Morphism_Theory.ind -cic:/matita/technicalities/setoids/Morphism_Context_rect2.con -cic:/matita/technicalities/setoids/Morphism_Context_rect.con -cic:/matita/technicalities/setoids/Morphism_Context_rec.con -cic:/matita/technicalities/setoids/Morphism_Context_inv.con -cic:/matita/technicalities/setoids/Morphism_Context_ind.con -cic:/matita/technicalities/setoids/Morphism_Context_List_rect2.con -cic:/matita/technicalities/setoids/Morphism_Context_List_rect.con -cic:/matita/technicalities/setoids/Morphism_Context_List_rec.con -cic:/matita/technicalities/setoids/Morphism_Context_List_inv.con -cic:/matita/technicalities/setoids/Morphism_Context_List_ind.con -cic:/matita/technicalities/setoids/Morphism_Context.ind -cic:/matita/technicalities/setoids/Impl_Relation_Class.con -cic:/matita/technicalities/setoids/Iff_Relation_Class.con -cic:/matita/technicalities/setoids/Function.con -cic:/matita/technicalities/setoids/Compat.con -cic:/matita/technicalities/setoids/Arguments.con -cic:/matita/technicalities/setoids/Argument_Class.con -cic:/matita/technicalities/setoids/Areflexive_Relation_Class_rect.con -cic:/matita/technicalities/setoids/Areflexive_Relation_Class_rec.con -cic:/matita/technicalities/setoids/Areflexive_Relation_Class_ind.con -cic:/matita/technicalities/setoids/Areflexive_Relation_Class.ind +# -- fine -- +# # the same fix in different contexts has different lamb-lifted counterpart + generative fix +# cic:/matita/demo/realisability/correct2.con +# cic:/matita/demo/realisability/correct.con +# cic:/matita/algebra/CoRN/SetoidFun/ap_fm_cotransitive.con +# # depending on the previous +# cic:/matita/algebra/CoRN/SemiGroups/Astar_is_CSemiGroup.con +# cic:/matita/algebra/CoRN/SemiGroups/Astar_as_CSemiGroup.con +# cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_is_CSetoid.con +# cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_as_csetoid.con +# cic:/matita/algebra/CoRN/SetoidFun/app_strext.con +# cic:/matita/algebra/CoRN/SetoidFun/app_as_csb_fun.con +# cic:/matita/algebra/CoRN/SetoidFun/appA.con +# cic:/matita/algebra/CoRN/SetoidFun/ap_fun.con +# cic:/matita/algebra/CoRN/SetoidFun/ap_fm_tight.con +# cic:/matita/algebra/CoRN/SetoidFun/ap_fm_symmetric.con +# cic:/matita/algebra/CoRN/SetoidFun/ap_fm_irreflexive.con +# cic:/matita/algebra/CoRN/SetoidFun/UR.con +# cic:/matita/algebra/CoRN/SetoidFun/UQ.con +# cic:/matita/algebra/CoRN/SetoidFun/UP.con +# cic:/matita/algebra/CoRN/SetoidFun/Tlist_rect.con +# cic:/matita/algebra/CoRN/SetoidFun/Tlist_rec.con +# cic:/matita/algebra/CoRN/SetoidFun/Tlist_ind.con +# cic:/matita/algebra/CoRN/SetoidFun/Tlist.ind +# cic:/matita/algebra/CoRN/SetoidFun/Tapp.con +# cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom1.con +# cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom.con +# cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom1.con +# cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom.con +# cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rect.con +# cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rec.con +# cic:/matita/algebra/CoRN/SetoidFun/PartFunct_ind.con +# cic:/matita/algebra/CoRN/SetoidFun/PartFunct.ind +# cic:/matita/algebra/CoRN/SetoidFun/Inv_bij.con +# cic:/matita/algebra/CoRN/SetoidFun/Inv.con +# cic:/matita/algebra/CoRN/SetoidFun/Fid.con +# cic:/matita/algebra/CoRN/SetoidFun/Fconst.con +# cic:/matita/algebra/CoRN/SetoidFun/Fcomp.con +# cic:/matita/algebra/CoRN/SetoidFun/FS_is_CSetoid.con +# cic:/matita/algebra/CoRN/SetoidFun/FS_as_CSetoid.con +# cic:/matita/algebra/CoRN/SetoidFun/Dir_bij.con +# cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rect.con +# cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rec.con +# cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_ind.con +# cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun.ind +# cic:/matita/algebra/CoRN/SetoidFun/CSap_fm.con +# cic:/matita/algebra/CoRN/SetoidFun/CAnd_rect.con +# cic:/matita/algebra/CoRN/SetoidFun/CAnd_rec.con +# cic:/matita/algebra/CoRN/SetoidFun/CAnd_ind.con +# cic:/matita/algebra/CoRN/SetoidFun/CAnd.ind +# cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rect.con +# cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rec.con +# cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_ind.con +# cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct.ind +# cic:/matita/algebra/CoRN/SetoidFun/BinFcomp.con +# cic:/matita/algebra/CoRN/SetoidFun/BR.con +# cic:/matita/algebra/CoRN/SetoidFun/BQ.con +# cic:/matita/algebra/CoRN/SetoidFun/BP.con +# cic:/matita/algebra/CoRN/SetoidFun/Astar.con +# # mutual fix +# cic:/matita/demo/propositional_sequent_calculus/not_nf_elim_not.con +# # depending on the previous +# cic:/matita/demo/propositional_sequent_calculus/eq_eval_elim_not_eval.con +# cic:/matita/demo/propositional_sequent_calculus/elim_not.con +# cic:/matita/demo/propositional_sequent_calculus/distributive_orb_andb.con +# cic:/matita/demo/propositional_sequent_calculus/distributive_andb_orb.con +# cic:/matita/demo/propositional_sequent_calculus/derive_inv.con +# cic:/matita/demo/propositional_sequent_calculus/derive_ind.con +# cic:/matita/demo/propositional_sequent_calculus/derive.ind +# cic:/matita/demo/propositional_sequent_calculus/demorgan2.con +# cic:/matita/demo/propositional_sequent_calculus/demorgan1.con +# cic:/matita/demo/propositional_sequent_calculus/daemon.con +# cic:/matita/demo/propositional_sequent_calculus/completeness_base.con +# cic:/matita/demo/propositional_sequent_calculus/associative_andb.con +# cic:/matita/demo/propositional_sequent_calculus/assoc_orb.con +# cic:/matita/demo/propositional_sequent_calculus/and_of_list_permut.con +# cic:/matita/demo/propositional_sequent_calculus/and_of_list.con +# cic:/matita/demo/propositional_sequent_calculus/Formula_rect.con +# cic:/matita/demo/propositional_sequent_calculus/Formula_rec.con +# cic:/matita/demo/propositional_sequent_calculus/Formula_ind.con +# cic:/matita/demo/propositional_sequent_calculus/Formula.ind +# # universe inferece missing +# cic:/matita/technicalities/setoids/relation_of_product_of_arguments.con +# cic:/matita/technicalities/setoids/product_of_arguments.con +# cic:/matita/technicalities/setoids/opposite_direction_idempotent.con +# cic:/matita/technicalities/setoids/opposite_direction.con +# cic:/matita/technicalities/setoids/nelistT_rect.con +# cic:/matita/technicalities/setoids/nelistT_rec.con +# cic:/matita/technicalities/setoids/nelistT_ind.con +# cic:/matita/technicalities/setoids/nelistT.ind +# cic:/matita/technicalities/setoids/morphism_theory_of_predicate.con +# cic:/matita/technicalities/setoids/morphism_theory_of_function.con +# cic:/matita/technicalities/setoids/make_compatibility_goal_aux.con +# cic:/matita/technicalities/setoids/make_compatibility_goal.con +# cic:/matita/technicalities/setoids/list_of_Leibniz_of_list_of_types.con +# cic:/matita/technicalities/setoids/interp_relation_class_list.con +# cic:/matita/technicalities/setoids/interp.con +# cic:/matita/technicalities/setoids/impl_trans.con +# cic:/matita/technicalities/setoids/impl_refl.con +# cic:/matita/technicalities/setoids/impl.con +# cic:/matita/technicalities/setoids/get_rewrite_direction.con +# cic:/matita/technicalities/setoids/function_type_of_morphism_signature.con +# cic:/matita/technicalities/setoids/equality_morphism_of_symmetric_reflexive_transitive_relation.con +# cic:/matita/technicalities/setoids/equality_morphism_of_symmetric_areflexive_transitive_relation.con +# cic:/matita/technicalities/setoids/equality_morphism_of_asymmetric_reflexive_transitive_relation.con +# cic:/matita/technicalities/setoids/equality_morphism_of_asymmetric_areflexive_transitive_relation.con +# cic:/matita/technicalities/setoids/directed_relation_of_relation_class.con +# cic:/matita/technicalities/setoids/directed_relation_of_argument_class.con +# cic:/matita/technicalities/setoids/check_if_variance_is_respected_inv.con +# cic:/matita/technicalities/setoids/check_if_variance_is_respected_ind.con +# cic:/matita/technicalities/setoids/check_if_variance_is_respected.ind +# cic:/matita/technicalities/setoids/carrier_of_relation_class.con +# cic:/matita/technicalities/setoids/carrier_of_reflexive_relation_class.con +# cic:/matita/technicalities/setoids/carrier_of_areflexive_relation_class.con +# cic:/matita/technicalities/setoids/apply_morphism_compatibility_Right2Left.con +# cic:/matita/technicalities/setoids/apply_morphism_compatibility_Left2Right.con +# cic:/matita/technicalities/setoids/apply_morphism.con +# cic:/matita/technicalities/setoids/about_carrier_of_relation_class_and_relation_class_of_argument_class.con +# cic:/matita/technicalities/setoids/X_Relation_Class_rect.con +# cic:/matita/technicalities/setoids/X_Relation_Class_rec.con +# cic:/matita/technicalities/setoids/X_Relation_Class_ind.con +# cic:/matita/technicalities/setoids/X_Relation_Class.ind +# cic:/matita/technicalities/setoids/Relation_Class.con +# cic:/matita/technicalities/setoids/Reflexive_Relation_Class_rect.con +# cic:/matita/technicalities/setoids/Reflexive_Relation_Class_rec.con +# cic:/matita/technicalities/setoids/Reflexive_Relation_Class_ind.con +# cic:/matita/technicalities/setoids/Reflexive_Relation_Class.ind +# cic:/matita/technicalities/setoids/Morphism_Theory_rect.con +# cic:/matita/technicalities/setoids/Morphism_Theory_rec.con +# cic:/matita/technicalities/setoids/Morphism_Theory_ind.con +# cic:/matita/technicalities/setoids/Morphism_Theory.ind +# cic:/matita/technicalities/setoids/Morphism_Context_rect2.con +# cic:/matita/technicalities/setoids/Morphism_Context_rect.con +# cic:/matita/technicalities/setoids/Morphism_Context_rec.con +# cic:/matita/technicalities/setoids/Morphism_Context_inv.con +# cic:/matita/technicalities/setoids/Morphism_Context_ind.con +# cic:/matita/technicalities/setoids/Morphism_Context_List_rect2.con +# cic:/matita/technicalities/setoids/Morphism_Context_List_rect.con +# cic:/matita/technicalities/setoids/Morphism_Context_List_rec.con +# cic:/matita/technicalities/setoids/Morphism_Context_List_inv.con +# cic:/matita/technicalities/setoids/Morphism_Context_List_ind.con +# cic:/matita/technicalities/setoids/Morphism_Context.ind +# cic:/matita/technicalities/setoids/Impl_Relation_Class.con +# cic:/matita/technicalities/setoids/Iff_Relation_Class.con +# cic:/matita/technicalities/setoids/Function.con +# cic:/matita/technicalities/setoids/Compat.con +# cic:/matita/technicalities/setoids/Arguments.con +# cic:/matita/technicalities/setoids/Argument_Class.con +# cic:/matita/technicalities/setoids/Areflexive_Relation_Class_rect.con +# cic:/matita/technicalities/setoids/Areflexive_Relation_Class_rec.con +# cic:/matita/technicalities/setoids/Areflexive_Relation_Class_ind.con +# cic:/matita/technicalities/setoids/Areflexive_Relation_Class.ind