-cic:/matita/Q/Qaxioms/symmetric_Qtimes.con
-cic:/matita/Q/Qaxioms/symmetric_Qplus.con
-cic:/matita/Q/Qaxioms/sigma_Q.con
-cic:/matita/Q/Qaxioms/num.con
-cic:/matita/Q/Qaxioms/frac_num_denom.con
-cic:/matita/Q/Qaxioms/frac_n.con
-cic:/matita/Q/Qaxioms/frac_Qopp.con
-cic:/matita/Q/Qaxioms/frac_Qinv2.con
-cic:/matita/Q/Qaxioms/frac_Qinv1.con
-cic:/matita/Q/Qaxioms/frac_O.con
-cic:/matita/Q/Qaxioms/frac.con
-cic:/matita/Q/Qaxioms/distributive_Qtimes_Qplus.con
-cic:/matita/Q/Qaxioms/denom.con
-cic:/matita/Q/Qaxioms/associative_Qtimes.con
-cic:/matita/Q/Qaxioms/associative_Qplus.con
-cic:/matita/Q/Qaxioms/Qtimes_frac.con
-cic:/matita/Q/Qaxioms/Qtimes_Qinv.con
-cic:/matita/Q/Qaxioms/Qtimes_Q1.con
-cic:/matita/Q/Qaxioms/Qtimes.con
-cic:/matita/Q/Qaxioms/Qplus_frac.con
-cic:/matita/Q/Qaxioms/Qplus_Qopp.con
-cic:/matita/Q/Qaxioms/Qplus_QO.con
-cic:/matita/Q/Qaxioms/Qplus.con
-cic:/matita/Q/Qaxioms/Qopp.con
-cic:/matita/Q/Qaxioms/Qlt_fracr.con
-cic:/matita/Q/Qaxioms/Qlt_fracl.con
-cic:/matita/Q/Qaxioms/Qlt.con
-cic:/matita/Q/Qaxioms/Qinv.con
-cic:/matita/Q/Qaxioms/QO.con
-cic:/matita/Q/Qaxioms/Q1.con
-cic:/matita/Q/Qaxioms/Q.con
-cic:/matita/Q/q/symmetric_rtimes.con
-cic:/matita/Q/q/symmetric2_ftimes.con
-cic:/matita/Q/q/rtimes_rinv.con
-cic:/matita/Q/q/rtimes.con
-cic:/matita/Q/q/rinv.con
-cic:/matita/Q/q/ratio_rect.con
-cic:/matita/Q/q/ratio_rec.con
-cic:/matita/Q/q/ratio_ind.con
-cic:/matita/Q/q/ratio.ind
-cic:/matita/Q/q/not_eq_pp_nn.con
-cic:/matita/Q/q/not_eq_pp_cons.con
-cic:/matita/Q/q/not_eq_nn_cons.con
-cic:/matita/Q/q/injective_pp.con
-cic:/matita/Q/q/injective_nn.con
-cic:/matita/Q/q/ftl.con
-cic:/matita/Q/q/ftimes_finv.con
-cic:/matita/Q/q/ftimes.con
-cic:/matita/Q/q/fraction_rect.con
-cic:/matita/Q/q/fraction_rec.con
-cic:/matita/Q/q/fraction_ind.con
-cic:/matita/Q/q/fraction_elim2.con
-cic:/matita/Q/q/fraction.ind
-cic:/matita/Q/q/finv.con
-cic:/matita/Q/q/fhd.con
-cic:/matita/Q/q/eqfb_to_Prop.con
-cic:/matita/Q/q/eqfb.con
-cic:/matita/Q/q/eq_cons_to_eq2.con
-cic:/matita/Q/q/eq_cons_to_eq1.con
-cic:/matita/Q/q/decidable_eq_fraction.con
-cic:/matita/Q/q/aux.con
-cic:/matita/Q/q/Z_to_ratio.con
-cic:/matita/Q/q/Qtimes.con
-cic:/matita/Q/q/Q_rect.con
-cic:/matita/Q/q/Q_rec.con
-cic:/matita/Q/q/Q_ind.con
-cic:/matita/Q/q/Q.ind
-cic:/matita/Z/compare/eqZb_to_Prop.con
-cic:/matita/Z/compare/eqZb_elim.con
-cic:/matita/Z/compare/eqZb.con
-cic:/matita/Z/compare/Z_compare_to_Prop.con
-cic:/matita/Z/compare/Z_compare.con
-cic:/matita/Z/dirichlet_product/sigma_p_OZ.con
-cic:/matita/Z/dirichlet_product/is_one_OZ.con
-cic:/matita/Z/dirichlet_product/is_one.con
-cic:/matita/Z/dirichlet_product/dirichlet_product_one_r.con
-cic:/matita/Z/dirichlet_product/dirichlet_product_one_l.con
-cic:/matita/Z/dirichlet_product/dirichlet_product_is_one_r.con
-cic:/matita/Z/dirichlet_product/dirichlet_product_is_one_l.con
-cic:/matita/Z/dirichlet_product/dirichlet_product.con
-cic:/matita/Z/dirichlet_product/commutative_dirichlet_product.con
-cic:/matita/Z/dirichlet_product/associative_dirichlet_product.con
-cic:/matita/Z/inversion/sigma_div_moebius.con
-cic:/matita/Z/inversion/sigma_div.con
-cic:/matita/Z/inversion/inversion.con
-cic:/matita/Z/moebius/sigma_p_moebius1.con
-cic:/matita/Z/moebius/sigma_p_moebius.con
-cic:/matita/Z/moebius/p_ord_SSq_r_to_moebius.con
-cic:/matita/Z/moebius/p_ord_SO_r_to_moebius1.con
-cic:/matita/Z/moebius/p_ord_SO_r_to_moebius.con
-cic:/matita/Z/moebius/p_ord_SO_SO_to_moebius.con
-cic:/matita/Z/moebius/not_divides_to_eq_moebius_aux.con
-cic:/matita/Z/moebius/moebius_exp.con
-cic:/matita/Z/moebius/moebius_aux_SO.con
-cic:/matita/Z/moebius/moebius_aux.con
-cic:/matita/Z/moebius/moebius.con
-cic:/matita/Z/moebius/eq_moebius_moebius_aux.con
-cic:/matita/Z/orders/transitive_Zlt.con
-cic:/matita/Z/orders/transitive_Zle.con
-cic:/matita/Z/orders/trans_Zlt.con
-cic:/matita/Z/orders/trans_Zle.con
-cic:/matita/Z/orders/lt_to_Zlt_pos_pos.con
-cic:/matita/Z/orders/lt_to_Zlt_neg_neg.con
-cic:/matita/Z/orders/irreflexive_Zlt.con
-cic:/matita/Z/orders/irrefl_Zlt.con
-cic:/matita/Z/orders/Zlt_to_Zle.con
-cic:/matita/Z/orders/Zlt_pos_pos_to_lt.con
-cic:/matita/Z/orders/Zlt_neg_neg_to_lt.con
-cic:/matita/Z/orders/Zlt.con
-cic:/matita/Z/orders/Zle.con
-cic:/matita/Z/plus/sym_Zplus.con
-cic:/matita/Z/plus/injective_Zplus_r.con
-cic:/matita/Z/plus/injective_Zplus_l.con
-cic:/matita/Z/plus/eq_OZ_Zopp_OZ.con
-cic:/matita/Z/plus/associative_Zplus.con
-cic:/matita/Z/plus/assoc_Zplus.con
-cic:/matita/Z/plus/Zsucc_Zplus_pos_O.con
-cic:/matita/Z/plus/Zpred_Zplus_neg_O.con
-cic:/matita/Z/plus/Zplus_z_OZ.con
-cic:/matita/Z/plus/Zplus_pos_pos.con
-cic:/matita/Z/plus/Zplus_pos_neg.con
-cic:/matita/Z/plus/Zplus_neg_pos.con
-cic:/matita/Z/plus/Zplus_neg_neg.con
-cic:/matita/Z/plus/Zplus_Zsucc_pos_pos.con
-cic:/matita/Z/plus/Zplus_Zsucc_pos_neg.con
-cic:/matita/Z/plus/Zplus_Zsucc_neg_pos.con
-cic:/matita/Z/plus/Zplus_Zsucc_neg_neg.con
-cic:/matita/Z/plus/Zplus_Zsucc_Zpred.con
-cic:/matita/Z/plus/Zplus_Zsucc.con
-cic:/matita/Z/plus/Zplus_Zpred.con
-cic:/matita/Z/plus/Zplus_Zopp.con
-cic:/matita/Z/plus/Zplus.con
-cic:/matita/Z/plus/Zopp_Zplus.con
-cic:/matita/Z/plus/Zopp_Zopp.con
-cic:/matita/Z/plus/Zopp.con
-cic:/matita/Z/plus/Zminus.con
-cic:/matita/Z/sigma_p/true_to_sigma_p_Sn.con
-cic:/matita/Z/sigma_p/symmetricZPlus.con
-cic:/matita/Z/sigma_p/sigma_p_plus.con
-cic:/matita/Z/sigma_p/sigma_p_knm.con
-cic:/matita/Z/sigma_p/sigma_p_gi.con
-cic:/matita/Z/sigma_p/sigma_p_false.con
-cic:/matita/Z/sigma_p/sigma_p_divides_b.con
-cic:/matita/Z/sigma_p/sigma_p2_eq.con
-cic:/matita/Z/sigma_p/sigma_p2.con
-cic:/matita/Z/sigma_p/sigma_p2'.con
-cic:/matita/Z/sigma_p/sigma_p.con
-cic:/matita/Z/sigma_p/false_to_sigma_p_Sn.con
-cic:/matita/Z/sigma_p/false_to_eq_sigma_p.con
-cic:/matita/Z/sigma_p/eq_sigma_p_gh.con
-cic:/matita/Z/sigma_p/eq_sigma_p1.con
-cic:/matita/Z/sigma_p/eq_sigma_p.con
-cic:/matita/Z/sigma_p/divides_exp_to_lt_ord.con
-cic:/matita/Z/sigma_p/divides_exp_to_divides_ord_rem.con
-cic:/matita/Z/sigma_p/Ztimes_sigma_pr.con
-cic:/matita/Z/sigma_p/Ztimes_sigma_pl.con
-cic:/matita/Z/times/times_minus1.con
-cic:/matita/Z/times/symmetric_Ztimes.con
-cic:/matita/Z/times/sym_Ztimes.con
-cic:/matita/Z/times/distributive_Ztimes_Zplus.con
-cic:/matita/Z/times/distributive2_Ztimes_pos_Zplus.con
-cic:/matita/Z/times/distributive2_Ztimes_neg_Zplus.con
-cic:/matita/Z/times/distr_Ztimes_Zplus_pos.con
-cic:/matita/Z/times/distr_Ztimes_Zplus_neg.con
-cic:/matita/Z/times/distr_Ztimes_Zplus.con
-cic:/matita/Z/times/associative_Ztimes.con
-cic:/matita/Z/times/assoc_Ztimes.con
-cic:/matita/Z/times/Ztimes_z_OZ.con
-cic:/matita/Z/times/Ztimes_neg_Zopp.con
-cic:/matita/Z/times/Ztimes_Zplus_pos_pos_neg.con
-cic:/matita/Z/times/Ztimes_Zplus_pos_neg_pos.con
-cic:/matita/Z/times/Ztimes_Zone_r.con
-cic:/matita/Z/times/Ztimes_Zone_l.con
-cic:/matita/Z/times/Ztimes.con
-cic:/matita/Z/times/Zone.con
-cic:/matita/Z/z/pos_n_eq_S_n.con
-cic:/matita/Z/z/not_eq_pos_neg.con
-cic:/matita/Z/z/not_eq_OZ_pos.con
-cic:/matita/Z/z/not_eq_OZ_neg.con
-cic:/matita/Z/z/neg_Z_of_nat.con
-cic:/matita/Z/z/injective_pos.con
-cic:/matita/Z/z/injective_neg.con
-cic:/matita/Z/z/inj_pos.con
-cic:/matita/Z/z/inj_neg.con
-cic:/matita/Z/z/decidable_eq_Z.con
-cic:/matita/Z/z/abs.con
-cic:/matita/Z/z/Zsucc_Zpred.con
-cic:/matita/Z/z/Zsucc.con
-cic:/matita/Z/z/Zpred_Zsucc.con
-cic:/matita/Z/z/Zpred.con
-cic:/matita/Z/z/Z_rect.con
-cic:/matita/Z/z/Z_rec.con
-cic:/matita/Z/z/Z_of_nat.con
-cic:/matita/Z/z/Z_ind.con
-cic:/matita/Z/z/Z.ind
-cic:/matita/Z/z/OZ_test_to_Prop.con
-cic:/matita/Z/z/OZ_test.con
-cic:/matita/algebra/CoRN/SemiGroups/subcrr.con
-cic:/matita/algebra/CoRN/SemiGroups/plus_assoc_unfolded.con
-cic:/matita/algebra/CoRN/SemiGroups/plus_assoc.con
-cic:/matita/algebra/CoRN/SemiGroups/part_function_plus_strext.con
-cic:/matita/algebra/CoRN/SemiGroups/morphism_of_CSemiGroups.con
-cic:/matita/algebra/CoRN/SemiGroups/mk_SubCSemiGroup.con
-cic:/matita/algebra/CoRN/SemiGroups/is_unit.con
-cic:/matita/algebra/CoRN/SemiGroups/is_rht_unit.con
-cic:/matita/algebra/CoRN/SemiGroups/is_lft_unit.con
-cic:/matita/algebra/CoRN/SemiGroups/is_CSemiGroup.con
-cic:/matita/algebra/CoRN/SemiGroups/included_FPlus.con
-cic:/matita/algebra/CoRN/SemiGroups/included_FPlus'.con
-cic:/matita/algebra/CoRN/SemiGroups/included_FPlus''.con
-cic:/matita/algebra/CoRN/SemiGroups/dprod_strext.con
-cic:/matita/algebra/CoRN/SemiGroups/dprod_as_csb_fun.con
-cic:/matita/algebra/CoRN/SemiGroups/dprod.con
-cic:/matita/algebra/CoRN/SemiGroups/direct_product_is_CSemiGroup.con
-cic:/matita/algebra/CoRN/SemiGroups/direct_product_as_CSemiGroup.con
-cic:/matita/algebra/CoRN/SemiGroups/csg_proof.con
-cic:/matita/algebra/CoRN/SemiGroups/csg_op.con
-cic:/matita/algebra/CoRN/SemiGroups/csg_crr.con
-cic:/matita/algebra/CoRN/SemiGroups/cs_unique_unit.con
-cic:/matita/algebra/CoRN/SemiGroups/Type_OF_CSemiGroup.con
-cic:/matita/algebra/CoRN/SemiGroups/NQ.con
-cic:/matita/algebra/CoRN/SemiGroups/NP.con
-cic:/matita/algebra/CoRN/SemiGroups/FunClass_2_OF_CSemiGroup.con
-cic:/matita/algebra/CoRN/SemiGroups/Fplus.con
-cic:/matita/algebra/CoRN/SemiGroups/FS_is_CSemiGroup.con
-cic:/matita/algebra/CoRN/SemiGroups/FS_as_CSemiGroup.con
-cic:/matita/algebra/CoRN/SemiGroups/CSemiGroup_rect.con
-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
-cic:/matita/algebra/CoRN/SetoidFun/surjective.con
-cic:/matita/algebra/CoRN/SetoidFun/sigT_rect.con
-cic:/matita/algebra/CoRN/SetoidFun/sigT_rec.con
-cic:/matita/algebra/CoRN/SetoidFun/sigT_ind.con
-cic:/matita/algebra/CoRN/SetoidFun/sigT.ind
-cic:/matita/algebra/CoRN/SetoidFun/projected_bin_fun.con
-cic:/matita/algebra/CoRN/SetoidFun/proj_bin_fun.con
-cic:/matita/algebra/CoRN/SetoidFun/projT2m.con
-cic:/matita/algebra/CoRN/SetoidFun/projT1.con
-cic:/matita/algebra/CoRN/SetoidFun/proj2_sigTm.con
-cic:/matita/algebra/CoRN/SetoidFun/proj1_sigT.con
-cic:/matita/algebra/CoRN/SetoidFun/prj2.con
-cic:/matita/algebra/CoRN/SetoidFun/prj1.con
-cic:/matita/algebra/CoRN/SetoidFun/pfwdef.con
-cic:/matita/algebra/CoRN/SetoidFun/pfstrx.con
-cic:/matita/algebra/CoRN/SetoidFun/pfpfun.con
-cic:/matita/algebra/CoRN/SetoidFun/pfdom.con
-cic:/matita/algebra/CoRN/SetoidFun/part_function_comp_strext.con
-cic:/matita/algebra/CoRN/SetoidFun/part_function_comp_dom_wd.con
-cic:/matita/algebra/CoRN/SetoidFun/opOnFun.con
-cic:/matita/algebra/CoRN/SetoidFun/n_ary_operation.con
-cic:/matita/algebra/CoRN/SetoidFun/mycor.con
-cic:/matita/algebra/CoRN/SetoidFun/is_nullary_operation.con
-cic:/matita/algebra/CoRN/SetoidFun/irrefl_apfun.con
-cic:/matita/algebra/CoRN/SetoidFun/invfun.con
-cic:/matita/algebra/CoRN/SetoidFun/inverse.con
-cic:/matita/algebra/CoRN/SetoidFun/inv_strext.con
-cic:/matita/algebra/CoRN/SetoidFun/inv2.con
-cic:/matita/algebra/CoRN/SetoidFun/inv1.con
-cic:/matita/algebra/CoRN/SetoidFun/injective_weak.con
-cic:/matita/algebra/CoRN/SetoidFun/injective_imp_injective_weak.con
-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
-cic:/matita/algebra/CoRN/SetoidFun/ext2.con
-cic:/matita/algebra/CoRN/SetoidFun/ext1.con
-cic:/matita/algebra/CoRN/SetoidFun/eq_to_ap_to_ap.con
-cic:/matita/algebra/CoRN/SetoidFun/eq_fun.con
-cic:/matita/algebra/CoRN/SetoidFun/eq_fm.con
-cic:/matita/algebra/CoRN/SetoidFun/empty_word.con
-cic:/matita/algebra/CoRN/SetoidFun/dom_wd.con
-cic:/matita/algebra/CoRN/SetoidFun/disj_wd.con
-cic:/matita/algebra/CoRN/SetoidFun/disj.con
-cic:/matita/algebra/CoRN/SetoidFun/direct.con
-cic:/matita/algebra/CoRN/SetoidFun/cs_binproj1.con
-cic:/matita/algebra/CoRN/SetoidFun/cotrans_apfun.con
-cic:/matita/algebra/CoRN/SetoidFun/conj_wd.con
-cic:/matita/algebra/CoRN/SetoidFun/conjP.con
-cic:/matita/algebra/CoRN/SetoidFun/compose_CSetoid_un_bin_fun.con
-cic:/matita/algebra/CoRN/SetoidFun/compose_CSetoid_fun.con
-cic:/matita/algebra/CoRN/SetoidFun/compose_CSetoid_bin_un_fun.con
-cic:/matita/algebra/CoRN/SetoidFun/compose_CSetoid_bin_fun.con
-cic:/matita/algebra/CoRN/SetoidFun/comp_resp_bij.con
-cic:/matita/algebra/CoRN/SetoidFun/comp_as_bin_op.con
-cic:/matita/algebra/CoRN/SetoidFun/comp.con
-cic:/matita/algebra/CoRN/SetoidFun/bpfwdef.con
-cic:/matita/algebra/CoRN/SetoidFun/bpfstrx.con
-cic:/matita/algebra/CoRN/SetoidFun/bpfpfun.con
-cic:/matita/algebra/CoRN/SetoidFun/bpfdom.con
-cic:/matita/algebra/CoRN/SetoidFun/block.con
-cic:/matita/algebra/CoRN/SetoidFun/binproj1_strext.con
-cic:/matita/algebra/CoRN/SetoidFun/binproj1.con
-cic:/matita/algebra/CoRN/SetoidFun/bin_part_function_comp_strext.con
-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
-cic:/matita/algebra/CoRN/SetoidInc/included_conj_rht.con
-cic:/matita/algebra/CoRN/SetoidInc/included_conj_lft.con
-cic:/matita/algebra/CoRN/SetoidInc/included_conj.con
-cic:/matita/algebra/CoRN/SetoidInc/included_conj'.con
-cic:/matita/algebra/CoRN/SetoidInc/included_conj''.con
-cic:/matita/algebra/CoRN/SetoidInc/included_FComp.con
-cic:/matita/algebra/CoRN/SetoidInc/included_FComp'.con
-cic:/matita/algebra/CoRN/SetoidInc/included.con
-cic:/matita/algebra/CoRN/Setoids/wdp_well_def.con
-cic:/matita/algebra/CoRN/Setoids/wdp_pred.con
-cic:/matita/algebra/CoRN/Setoids/wd_pred_rect.con
-cic:/matita/algebra/CoRN/Setoids/wd_pred_rec.con
-cic:/matita/algebra/CoRN/Setoids/wd_pred_ind.con
-cic:/matita/algebra/CoRN/Setoids/wd_pred.ind
-cic:/matita/algebra/CoRN/Setoids/un_op_wd_unfolded.con
-cic:/matita/algebra/CoRN/Setoids/un_op_wd.con
-cic:/matita/algebra/CoRN/Setoids/un_op_strext_unfolded.con
-cic:/matita/algebra/CoRN/Setoids/un_op_strext.con
-cic:/matita/algebra/CoRN/Setoids/un_op_pres_pred.con
-cic:/matita/algebra/CoRN/Setoids/un_op_fun.con
-cic:/matita/algebra/CoRN/Setoids/subcsetoid_is_CSetoid.con
-cic:/matita/algebra/CoRN/Setoids/subcsetoid_equiv.con
-cic:/matita/algebra/CoRN/Setoids/subcsetoid_eq.con
-cic:/matita/algebra/CoRN/Setoids/subcsetoid_crr_rect.con
-cic:/matita/algebra/CoRN/Setoids/subcsetoid_crr_rec.con
-cic:/matita/algebra/CoRN/Setoids/subcsetoid_crr_ind.con
-cic:/matita/algebra/CoRN/Setoids/subcsetoid_crr.ind
-cic:/matita/algebra/CoRN/Setoids/subcsetoid_ap.con
-cic:/matita/algebra/CoRN/Setoids/scs_prf.con
-cic:/matita/algebra/CoRN/Setoids/scs_elem.con
-cic:/matita/algebra/CoRN/Setoids/restrict_relation.con
-cic:/matita/algebra/CoRN/Setoids/restr_un_op_wd.con
-cic:/matita/algebra/CoRN/Setoids/restr_un_op_strext.con
-cic:/matita/algebra/CoRN/Setoids/restr_un_op.con
-cic:/matita/algebra/CoRN/Setoids/restr_f_assoc.con
-cic:/matita/algebra/CoRN/Setoids/restr_bin_op_well_def.con
-cic:/matita/algebra/CoRN/Setoids/restr_bin_op_strext.con
-cic:/matita/algebra/CoRN/Setoids/restr_bin_op.con
-cic:/matita/algebra/CoRN/Setoids/rel_wdr.con
-cic:/matita/algebra/CoRN/Setoids/rel_wdl.con
-cic:/matita/algebra/CoRN/Setoids/rel_strextarg_imp_strext.con
-cic:/matita/algebra/CoRN/Setoids/rel_strext_rht.con
-cic:/matita/algebra/CoRN/Setoids/rel_strext_lft.con
-cic:/matita/algebra/CoRN/Setoids/rel_strext_imp_rhtarg.con
-cic:/matita/algebra/CoRN/Setoids/rel_strext_imp_lftarg.con
-cic:/matita/algebra/CoRN/Setoids/rel_strext.con
-cic:/matita/algebra/CoRN/Setoids/proper_caseZ_diff_CS.con
-cic:/matita/algebra/CoRN/Setoids/prodcsetoid_is_CSetoid.con
-cic:/matita/algebra/CoRN/Setoids/prod_eq.con
-cic:/matita/algebra/CoRN/Setoids/prod_ap.con
-cic:/matita/algebra/CoRN/Setoids/pred_wd.con
-cic:/matita/algebra/CoRN/Setoids/pred_strong_ext.con
-cic:/matita/algebra/CoRN/Setoids/outer_op_well_def.con
-cic:/matita/algebra/CoRN/Setoids/outer_op_strext.con
-cic:/matita/algebra/CoRN/Setoids/outer_op_bin_fun.con
-cic:/matita/algebra/CoRN/Setoids/notnot_ap_imp_neq.con
-cic:/matita/algebra/CoRN/Setoids/not_neq_imp_eq.con
-cic:/matita/algebra/CoRN/Setoids/not_ap_imp_eq.con
-cic:/matita/algebra/CoRN/Setoids/neq_imp_notnot_ap.con
-cic:/matita/algebra/CoRN/Setoids/nat_less_n_fun.con
-cic:/matita/algebra/CoRN/Setoids/nat_less_n_fun'.con
-cic:/matita/algebra/CoRN/Setoids/mk_SubCSetoid_un_op.con
-cic:/matita/algebra/CoRN/Setoids/mk_SubCSetoid_bin_op.con
-cic:/matita/algebra/CoRN/Setoids/mk_SubCSetoid.con
-cic:/matita/algebra/CoRN/Setoids/mk_CSetoid_un_op.con
-cic:/matita/algebra/CoRN/Setoids/mk_CSetoid_outer_op.con
-cic:/matita/algebra/CoRN/Setoids/mk_CSetoid_bin_op.con
-cic:/matita/algebra/CoRN/Setoids/is_CSetoid_rect.con
-cic:/matita/algebra/CoRN/Setoids/is_CSetoid_rec.con
-cic:/matita/algebra/CoRN/Setoids/is_CSetoid_ind.con
-cic:/matita/algebra/CoRN/Setoids/is_CSetoid.ind
-cic:/matita/algebra/CoRN/Setoids/id_un_op.con
-cic:/matita/algebra/CoRN/Setoids/id_strext.con
-cic:/matita/algebra/CoRN/Setoids/id_pres_eq.con
-cic:/matita/algebra/CoRN/Setoids/fun_wd.con
-cic:/matita/algebra/CoRN/Setoids/fun_strext_imp_wd.con
-cic:/matita/algebra/CoRN/Setoids/fun_strext.con
-cic:/matita/algebra/CoRN/Setoids/ex_unq.con
-cic:/matita/algebra/CoRN/Setoids/equiv.con
-cic:/matita/algebra/CoRN/Setoids/eq_wdl.con
-cic:/matita/algebra/CoRN/Setoids/eq_transitive_unfolded.con
-cic:/matita/algebra/CoRN/Setoids/eq_transitive.con
-cic:/matita/algebra/CoRN/Setoids/eq_symmetric_unfolded.con
-cic:/matita/algebra/CoRN/Setoids/eq_symmetric.con
-cic:/matita/algebra/CoRN/Setoids/eq_reflexive_unfolded.con
-cic:/matita/algebra/CoRN/Setoids/eq_reflexive.con
-cic:/matita/algebra/CoRN/Setoids/eq_imp_not_neq.con
-cic:/matita/algebra/CoRN/Setoids/eq_imp_not_ap.con
-cic:/matita/algebra/CoRN/Setoids/csp_wd.con
-cic:/matita/algebra/CoRN/Setoids/csp_strext.con
-cic:/matita/algebra/CoRN/Setoids/csp_pred.con
-cic:/matita/algebra/CoRN/Setoids/csoo_wd_unfolded.con
-cic:/matita/algebra/CoRN/Setoids/csoo_wd.con
-cic:/matita/algebra/CoRN/Setoids/csoo_strext.con
-cic:/matita/algebra/CoRN/Setoids/csf_wd_unfolded.con
-cic:/matita/algebra/CoRN/Setoids/csf_wd.con
-cic:/matita/algebra/CoRN/Setoids/csf_strext_unfolded.con
-cic:/matita/algebra/CoRN/Setoids/csf_strext.con
-cic:/matita/algebra/CoRN/Setoids/csf_fun.con
-cic:/matita/algebra/CoRN/Setoids/csbf_wd_unfolded.con
-cic:/matita/algebra/CoRN/Setoids/csbf_wd.con
-cic:/matita/algebra/CoRN/Setoids/csbf_strext.con
-cic:/matita/algebra/CoRN/Setoids/csbf_fun.con
-cic:/matita/algebra/CoRN/Setoids/cs_un_op_strext.con
-cic:/matita/algebra/CoRN/Setoids/cs_proof.con
-cic:/matita/algebra/CoRN/Setoids/cs_neq.con
-cic:/matita/algebra/CoRN/Setoids/cs_eq.con
-cic:/matita/algebra/CoRN/Setoids/cs_crr.con
-cic:/matita/algebra/CoRN/Setoids/cs_bin_op_wd.con
-cic:/matita/algebra/CoRN/Setoids/cs_bin_op_strext.con
-cic:/matita/algebra/CoRN/Setoids/cs_ap.con
-cic:/matita/algebra/CoRN/Setoids/commutes.con
-cic:/matita/algebra/CoRN/Setoids/caseZ_diff.con
-cic:/matita/algebra/CoRN/Setoids/bin_op_wd_unfolded.con
-cic:/matita/algebra/CoRN/Setoids/bin_op_wd.con
-cic:/matita/algebra/CoRN/Setoids/bin_op_strext_unfolded.con
-cic:/matita/algebra/CoRN/Setoids/bin_op_strext.con
-cic:/matita/algebra/CoRN/Setoids/bin_op_pres_pred.con
-cic:/matita/algebra/CoRN/Setoids/bin_op_is_wd_un_op_rht.con
-cic:/matita/algebra/CoRN/Setoids/bin_op_is_wd_un_op_lft.con
-cic:/matita/algebra/CoRN/Setoids/bin_op_is_strext_un_op_rht.con
-cic:/matita/algebra/CoRN/Setoids/bin_op_is_strext_un_op_lft.con
-cic:/matita/algebra/CoRN/Setoids/bin_op_bin_fun.con
-cic:/matita/algebra/CoRN/Setoids/bin_op2un_op_rht.con
-cic:/matita/algebra/CoRN/Setoids/bin_op2un_op_lft.con
-cic:/matita/algebra/CoRN/Setoids/bin_fun_wd.con
-cic:/matita/algebra/CoRN/Setoids/bin_fun_strext_imp_wd.con
-cic:/matita/algebra/CoRN/Setoids/bin_fun_strext.con
-cic:/matita/algebra/CoRN/Setoids/ax_ap_tight.con
-cic:/matita/algebra/CoRN/Setoids/ax_ap_symmetric.con
-cic:/matita/algebra/CoRN/Setoids/ax_ap_irreflexive.con
-cic:/matita/algebra/CoRN/Setoids/ax_ap_cotransitive.con
-cic:/matita/algebra/CoRN/Setoids/ap_tight.con
-cic:/matita/algebra/CoRN/Setoids/ap_symmetric_unfolded.con
-cic:/matita/algebra/CoRN/Setoids/ap_symmetric.con
-cic:/matita/algebra/CoRN/Setoids/ap_irreflexive_unfolded.con
-cic:/matita/algebra/CoRN/Setoids/ap_irreflexive.con
-cic:/matita/algebra/CoRN/Setoids/ap_imp_neq.con
-cic:/matita/algebra/CoRN/Setoids/ap_cotransitive_unfolded.con
-cic:/matita/algebra/CoRN/Setoids/ap_cotransitive.con
-cic:/matita/algebra/CoRN/Setoids/Zminus_S_S.con
-cic:/matita/algebra/CoRN/Setoids/Prop_OF_subcsetoid_crr1.con
-cic:/matita/algebra/CoRN/Setoids/Prop_OF_subcsetoid_crr.con
-cic:/matita/algebra/CoRN/Setoids/ProdCSetoid.con
-cic:/matita/algebra/CoRN/Setoids/FunClass_2_OF_CSetoid_outer_op.con
-cic:/matita/algebra/CoRN/Setoids/FunClass_2_OF_CSetoid_bin_op.con
-cic:/matita/algebra/CoRN/Setoids/Const_CSetoid_fun.con
-cic:/matita/algebra/CoRN/Setoids/CSetoid_un_op.con
-cic:/matita/algebra/CoRN/Setoids/CSetoid_rect.con
-cic:/matita/algebra/CoRN/Setoids/CSetoid_rec.con
-cic:/matita/algebra/CoRN/Setoids/CSetoid_predicate_rect.con
-cic:/matita/algebra/CoRN/Setoids/CSetoid_predicate_rec.con
-cic:/matita/algebra/CoRN/Setoids/CSetoid_predicate_ind.con
-cic:/matita/algebra/CoRN/Setoids/CSetoid_predicate.ind
-cic:/matita/algebra/CoRN/Setoids/CSetoid_outer_op.con
-cic:/matita/algebra/CoRN/Setoids/CSetoid_is_CSetoid.con
-cic:/matita/algebra/CoRN/Setoids/CSetoid_ind.con
-cic:/matita/algebra/CoRN/Setoids/CSetoid_fun_rect.con
-cic:/matita/algebra/CoRN/Setoids/CSetoid_fun_rec.con
-cic:/matita/algebra/CoRN/Setoids/CSetoid_fun_ind.con
-cic:/matita/algebra/CoRN/Setoids/CSetoid_fun.ind
-cic:/matita/algebra/CoRN/Setoids/CSetoid_bin_op.con
-cic:/matita/algebra/CoRN/Setoids/CSetoid_bin_fun_rect.con
-cic:/matita/algebra/CoRN/Setoids/CSetoid_bin_fun_rec.con
-cic:/matita/algebra/CoRN/Setoids/CSetoid_bin_fun_ind.con
-cic:/matita/algebra/CoRN/Setoids/CSetoid_bin_fun.ind
-cic:/matita/algebra/CoRN/Setoids/CSetoid.ind
-cic:/matita/algebra/CoRN/Setoids/CSassociative.con
-cic:/matita/algebra/finite_groups/semigroup.con
-cic:/matita/algebra/finite_groups/repr_index_of.con
-cic:/matita/algebra/finite_groups/repr.con
-cic:/matita/algebra/finite_groups/pigeonhole.con
-cic:/matita/algebra/finite_groups/order.con
-cic:/matita/algebra/finite_groups/is_finite_enumerable.con
-cic:/matita/algebra/finite_groups/isSemiGroup_OF_finite_enumerable_SemiGroup.con
-cic:/matita/algebra/finite_groups/index_of_sur.con
-cic:/matita/algebra/finite_groups/index_of_repr.con
-cic:/matita/algebra/finite_groups/index_of.con
-cic:/matita/algebra/finite_groups/finite_enumerable_rect.con
-cic:/matita/algebra/finite_groups/finite_enumerable_rec.con
-cic:/matita/algebra/finite_groups/finite_enumerable_ind.con
-cic:/matita/algebra/finite_groups/finite_enumerable_SemiGroup_to_left_cancellable_to_right_cancellable_to_isMonoid.con
-cic:/matita/algebra/finite_groups/finite_enumerable_SemiGroup_rect.con
-cic:/matita/algebra/finite_groups/finite_enumerable_SemiGroup_rec.con
-cic:/matita/algebra/finite_groups/finite_enumerable_SemiGroup_ind.con
-cic:/matita/algebra/finite_groups/finite_enumerable_SemiGroup.ind
-cic:/matita/algebra/finite_groups/finite_enumerable.ind
-cic:/matita/algebra/finite_groups/Type_OF_finite_enumerable_SemiGroup.con
-cic:/matita/algebra/finite_groups/Magma_OF_finite_enumerable_SemiGroup.con
-cic:/matita/algebra/groups/subgrp.con
-cic:/matita/algebra/groups/subgroup_rect.con
-cic:/matita/algebra/groups/subgroup_rec.con
-cic:/matita/algebra/groups/subgroup_ind.con
-cic:/matita/algebra/groups/subgroup.ind
-cic:/matita/algebra/groups/right_cancellable.con
-cic:/matita/algebra/groups/premonoid.con
-cic:/matita/algebra/groups/pregroup.con
-cic:/matita/algebra/groups/ns_subgroup.con
-cic:/matita/algebra/groups/normal_subgroup_rect.con
-cic:/matita/algebra/groups/normal_subgroup_rec.con
-cic:/matita/algebra/groups/normal_subgroup_ind.con
-cic:/matita/algebra/groups/normal_subgroup.ind
-cic:/matita/algebra/groups/normal.con
-cic:/matita/algebra/groups/morphism_to_eq_f_1_1.con
-cic:/matita/algebra/groups/morphism_rect.con
-cic:/matita/algebra/groups/morphism_rec.con
-cic:/matita/algebra/groups/morphism_ind.con
-cic:/matita/algebra/groups/morphism_OF_subgroup.con
-cic:/matita/algebra/groups/morphism_OF_normal_subgroup.con
-cic:/matita/algebra/groups/morphism.ind
-cic:/matita/algebra/groups/morphism.con
-cic:/matita/algebra/groups/monomorphism_rect.con
-cic:/matita/algebra/groups/monomorphism_rec.con
-cic:/matita/algebra/groups/monomorphism_ind.con
-cic:/matita/algebra/groups/monomorphism_OF_normal_subgroup.con
-cic:/matita/algebra/groups/monomorphism.ind
-cic:/matita/algebra/groups/member_of_subgroup_op_inv_x_y_to_left_coset_eq.con
-cic:/matita/algebra/groups/member_of_subgroup.con
-cic:/matita/algebra/groups/member_of_left_coset.con
-cic:/matita/algebra/groups/left_coset_rect.con
-cic:/matita/algebra/groups/left_coset_rec.con
-cic:/matita/algebra/groups/left_coset_ind.con
-cic:/matita/algebra/groups/left_coset_eq.con
-cic:/matita/algebra/groups/left_coset_disjoint.con
-cic:/matita/algebra/groups/left_coset.ind
-cic:/matita/algebra/groups/left_cancellable.con
-cic:/matita/algebra/groups/is_monoid.con
-cic:/matita/algebra/groups/isSemiGroup_OF_subgroup.con
-cic:/matita/algebra/groups/isSemiGroup_OF_normal_subgroup.con
-cic:/matita/algebra/groups/isSemiGroup_OF_isGroup.con
-cic:/matita/algebra/groups/isSemiGroup_OF_Group.con
-cic:/matita/algebra/groups/isMonoid_OF_subgroup.con
-cic:/matita/algebra/groups/isMonoid_OF_normal_subgroup.con
-cic:/matita/algebra/groups/isMonoid_OF_Group.con
-cic:/matita/algebra/groups/isGroup_rect.con
-cic:/matita/algebra/groups/isGroup_rec.con
-cic:/matita/algebra/groups/isGroup_ind.con
-cic:/matita/algebra/groups/isGroup_OF_subgroup.con
-cic:/matita/algebra/groups/isGroup_OF_normal_subgroup.con
-cic:/matita/algebra/groups/isGroup.ind
-cic:/matita/algebra/groups/inv_is_right_inverse.con
-cic:/matita/algebra/groups/inv_is_left_inverse.con
-cic:/matita/algebra/groups/inv.con
-cic:/matita/algebra/groups/injective.con
-cic:/matita/algebra/groups/in_x_mk_left_coset_x_H.con
-cic:/matita/algebra/groups/image.con
-cic:/matita/algebra/groups/group_properties.con
-cic:/matita/algebra/groups/group.con
-cic:/matita/algebra/groups/f_morph.con
-cic:/matita/algebra/groups/eq_opxy_z_to_eq_y_opinvxz.con
-cic:/matita/algebra/groups/eq_opxy_z_to_eq_x_opzinvy.con
-cic:/matita/algebra/groups/eq_opxy_e_to_eq_x_invy.con
-cic:/matita/algebra/groups/eq_opxy_e_to_eq_invx_y.con
-cic:/matita/algebra/groups/eq_op_x_y_op_z_y_to_eq.con
-cic:/matita/algebra/groups/eq_op_x_y_op_x_z_to_eq.con
-cic:/matita/algebra/groups/eq_inv_op_x_y_op_inv_y_inv_x.con
-cic:/matita/algebra/groups/eq_inv_inv_x_x.con
-cic:/matita/algebra/groups/eq_image_inv_inv_image.con
-cic:/matita/algebra/groups/embed.con
-cic:/matita/algebra/groups/element.con
-cic:/matita/algebra/groups/Type_OF_subgroup.con
-cic:/matita/algebra/groups/Type_OF_normal_subgroup.con
-cic:/matita/algebra/groups/Type_OF_PreGroup.con
-cic:/matita/algebra/groups/Type_OF_Group.con
-cic:/matita/algebra/groups/PreMonoid_OF_subgroup.con
-cic:/matita/algebra/groups/PreMonoid_OF_normal_subgroup.con
-cic:/matita/algebra/groups/PreMonoid_OF_Group.con
-cic:/matita/algebra/groups/PreGroup_rect.con
-cic:/matita/algebra/groups/PreGroup_rec.con
-cic:/matita/algebra/groups/PreGroup_ind.con
-cic:/matita/algebra/groups/PreGroup_OF_subgroup.con
-cic:/matita/algebra/groups/PreGroup_OF_normal_subgroup.con
-cic:/matita/algebra/groups/PreGroup.ind
-cic:/matita/algebra/groups/Not_member_of_subgroup_to_left_coset_disjoint.con
-cic:/matita/algebra/groups/Magma_OF_subgroup.con
-cic:/matita/algebra/groups/Magma_OF_normal_subgroup.con
-cic:/matita/algebra/groups/Magma_OF_PreGroup.con
-cic:/matita/algebra/groups/Magma_OF_Group.con
-cic:/matita/algebra/groups/Group_rect.con
-cic:/matita/algebra/groups/Group_rec.con
-cic:/matita/algebra/groups/Group_ind.con
-cic:/matita/algebra/groups/Group_OF_normal_subgroup.con
-cic:/matita/algebra/groups/Group.ind
-cic:/matita/algebra/monoids/premonoid.con
-cic:/matita/algebra/monoids/monoid_properties.con
-cic:/matita/algebra/monoids/magma.con
-cic:/matita/algebra/monoids/is_semi_group.con
-cic:/matita/algebra/monoids/is_right_inverse.con
-cic:/matita/algebra/monoids/is_left_inverse_to_is_right_inverse_to_eq.con
-cic:/matita/algebra/monoids/is_left_inverse.con
-cic:/matita/algebra/monoids/isSemiGroup_OF_Monoid.con
-cic:/matita/algebra/monoids/isMonoid_rect.con
-cic:/matita/algebra/monoids/isMonoid_rec.con
-cic:/matita/algebra/monoids/isMonoid_ind.con
-cic:/matita/algebra/monoids/isMonoid.ind
-cic:/matita/algebra/monoids/e_is_right_unit.con
-cic:/matita/algebra/monoids/e_is_left_unit.con
-cic:/matita/algebra/monoids/e.con
-cic:/matita/algebra/monoids/Type_OF_PreMonoid.con
-cic:/matita/algebra/monoids/Type_OF_Monoid.con
-cic:/matita/algebra/monoids/PreMonoid_rect.con
-cic:/matita/algebra/monoids/PreMonoid_rec.con
-cic:/matita/algebra/monoids/PreMonoid_ind.con
-cic:/matita/algebra/monoids/PreMonoid.ind
-cic:/matita/algebra/monoids/Monoid_rect.con
-cic:/matita/algebra/monoids/Monoid_rec.con
-cic:/matita/algebra/monoids/Monoid_ind.con
-cic:/matita/algebra/monoids/Monoid.ind
-cic:/matita/algebra/monoids/Magma_OF_Monoid.con
-cic:/matita/algebra/semigroups/semigroup_properties.con
-cic:/matita/algebra/semigroups/op_associative.con
-cic:/matita/algebra/semigroups/op.con
-cic:/matita/algebra/semigroups/magma.con
-cic:/matita/algebra/semigroups/is_right_unit.con
-cic:/matita/algebra/semigroups/is_left_unit_to_is_right_unit_to_eq.con
-cic:/matita/algebra/semigroups/is_left_unit.con
-cic:/matita/algebra/semigroups/isSemiGroup_rect.con
-cic:/matita/algebra/semigroups/isSemiGroup_rec.con
-cic:/matita/algebra/semigroups/isSemiGroup_ind.con
-cic:/matita/algebra/semigroups/isSemiGroup.ind
-cic:/matita/algebra/semigroups/carrier.con
-cic:/matita/algebra/semigroups/Type_OF_SemiGroup.con
-cic:/matita/algebra/semigroups/SemiGroup_rect.con
-cic:/matita/algebra/semigroups/SemiGroup_rec.con
-cic:/matita/algebra/semigroups/SemiGroup_ind.con
-cic:/matita/algebra/semigroups/SemiGroup.ind
-cic:/matita/algebra/semigroups/Magma_rect.con
-cic:/matita/algebra/semigroups/Magma_rec.con
-cic:/matita/algebra/semigroups/Magma_ind.con
-cic:/matita/algebra/semigroups/Magma.ind
-cic:/matita/datatypes/bool/true_to_true_to_andb_true.con
-cic:/matita/datatypes/bool/orb_sym.con
-cic:/matita/datatypes/bool/orb_elim.con
-cic:/matita/datatypes/bool/orb.con
-cic:/matita/datatypes/bool/notb_notb.con
-cic:/matita/datatypes/bool/notb_elim.con
-cic:/matita/datatypes/bool/notb.con
-cic:/matita/datatypes/bool/not_eq_true_false.con
-cic:/matita/datatypes/bool/injective_notb.con
-cic:/matita/datatypes/bool/if_then_else.con
-cic:/matita/datatypes/bool/bool_to_decidable_eq.con
-cic:/matita/datatypes/bool/bool_rect.con
-cic:/matita/datatypes/bool/bool_rec.con
-cic:/matita/datatypes/bool/bool_ind.con
-cic:/matita/datatypes/bool/bool_elim.con
-cic:/matita/datatypes/bool/bool.ind
-cic:/matita/datatypes/bool/andb_true_true_r.con
-cic:/matita/datatypes/bool/andb_true_true.con
-cic:/matita/datatypes/bool/andb_sym.con
-cic:/matita/datatypes/bool/andb_elim.con
-cic:/matita/datatypes/bool/andb_assoc.con
-cic:/matita/datatypes/bool/andb.con
-cic:/matita/datatypes/bool/and_true.con
-cic:/matita/datatypes/bool/P_x_to_P_x_to_eq.con
-cic:/matita/datatypes/compare/compare_rect.con
-cic:/matita/datatypes/compare/compare_rec.con
-cic:/matita/datatypes/compare/compare_invert.con
-cic:/matita/datatypes/compare/compare_ind.con
-cic:/matita/datatypes/compare/compare.ind
-cic:/matita/datatypes/constructors/void_rect.con
-cic:/matita/datatypes/constructors/void_rec.con
-cic:/matita/datatypes/constructors/void_ind.con
-cic:/matita/datatypes/constructors/void.ind
-cic:/matita/datatypes/constructors/unit_rect.con
-cic:/matita/datatypes/constructors/unit_rec.con
-cic:/matita/datatypes/constructors/unit_ind.con
-cic:/matita/datatypes/constructors/unit.ind
-cic:/matita/datatypes/constructors/snd.con
-cic:/matita/datatypes/constructors/option_rect.con
-cic:/matita/datatypes/constructors/option_rec.con
-cic:/matita/datatypes/constructors/option_ind.con
-cic:/matita/datatypes/constructors/option.ind
-cic:/matita/datatypes/constructors/fst.con
-cic:/matita/datatypes/constructors/eq_pair_fst_snd.con
-cic:/matita/datatypes/constructors/Sum_rect.con
-cic:/matita/datatypes/constructors/Sum_rec.con
-cic:/matita/datatypes/constructors/Sum_ind.con
-cic:/matita/datatypes/constructors/Sum.ind
-cic:/matita/datatypes/constructors/Prod_rect.con
-cic:/matita/datatypes/constructors/Prod_rec.con
-cic:/matita/datatypes/constructors/Prod_ind.con
-cic:/matita/datatypes/constructors/Prod.ind
-cic:/matita/decidable_kit/decidable/reflect_rect.con
-cic:/matita/decidable_kit/decidable/reflect_rec.con
-cic:/matita/decidable_kit/decidable/reflect_inv.con
-cic:/matita/decidable_kit/decidable/reflect_ind.con
-cic:/matita/decidable_kit/decidable/reflect.ind
-cic:/matita/decidable_kit/decidable/prove_reflect.con
-cic:/matita/decidable_kit/decidable/p2bT.con
-cic:/matita/decidable_kit/decidable/p2bF.con
-cic:/matita/decidable_kit/decidable/orbP.con
-cic:/matita/decidable_kit/decidable/orbC.con
-cic:/matita/decidable_kit/decidable/orb.con
-cic:/matita/decidable_kit/decidable/negbP.con
-cic:/matita/decidable_kit/decidable/negb.con
-cic:/matita/decidable_kit/decidable/ltb_refl.con
-cic:/matita/decidable_kit/decidable/ltb_n_Sm.con
-cic:/matita/decidable_kit/decidable/ltbW.con
-cic:/matita/decidable_kit/decidable/ltbP.con
-cic:/matita/decidable_kit/decidable/ltb.con
-cic:/matita/decidable_kit/decidable/ltW.con
-cic:/matita/decidable_kit/decidable/ltS.con
-cic:/matita/decidable_kit/decidable/ltS'.con
-cic:/matita/decidable_kit/decidable/leb_refl.con
-cic:/matita/decidable_kit/decidable/leb_eqb.con
-cic:/matita/decidable_kit/decidable/lebW.con
-cic:/matita/decidable_kit/decidable/lebP.con
-cic:/matita/decidable_kit/decidable/idP.con
-cic:/matita/decidable_kit/decidable/eq_to_bool.con
-cic:/matita/decidable_kit/decidable/congr_S.con
-cic:/matita/decidable_kit/decidable/bool_to_eq.con
-cic:/matita/decidable_kit/decidable/b2pT.con
-cic:/matita/decidable_kit/decidable/b2pF.con
-cic:/matita/decidable_kit/decidable/andbPF.con
-cic:/matita/decidable_kit/decidable/andbP.con
-cic:/matita/decidable_kit/decidable/andb.con
-cic:/matita/decidable_kit/eqtype/test_canonical_option_eqType.con
-cic:/matita/decidable_kit/eqtype/sval.con
-cic:/matita/decidable_kit/eqtype/sub_eqType.con
-cic:/matita/decidable_kit/eqtype/sprop.con
-cic:/matita/decidable_kit/eqtype/sort_OF_nat.con
-cic:/matita/decidable_kit/eqtype/sort_OF_bool.con
-cic:/matita/decidable_kit/eqtype/sort.con
-cic:/matita/decidable_kit/eqtype/sigma_rect.con
-cic:/matita/decidable_kit/eqtype/sigma_rec.con
-cic:/matita/decidable_kit/eqtype/sigma_ind.con
-cic:/matita/decidable_kit/eqtype/sigma_eq_dec.con
-cic:/matita/decidable_kit/eqtype/sigma.ind
-cic:/matita/decidable_kit/eqtype/option_eqType.con
-cic:/matita/decidable_kit/eqtype/option_canonical_eqType.con
-cic:/matita/decidable_kit/eqtype/ocmpP.con
-cic:/matita/decidable_kit/eqtype/ocmp.con
-cic:/matita/decidable_kit/eqtype/nat_eqType.con
-cic:/matita/decidable_kit/eqtype/nat_canonical_eqType.con
-cic:/matita/decidable_kit/eqtype/in_sub_rect.con
-cic:/matita/decidable_kit/eqtype/in_sub_rec.con
-cic:/matita/decidable_kit/eqtype/in_sub_inv.con
-cic:/matita/decidable_kit/eqtype/in_sub_ind.con
-cic:/matita/decidable_kit/eqtype/in_sub_eq.con
-cic:/matita/decidable_kit/eqtype/in_sub.ind
-cic:/matita/decidable_kit/eqtype/if_p.con
-cic:/matita/decidable_kit/eqtype/eqbP.con
-cic:/matita/decidable_kit/eqtype/eq_compatible.con
-cic:/matita/decidable_kit/eqtype/eqType_rect.con
-cic:/matita/decidable_kit/eqtype/eqType_rec.con
-cic:/matita/decidable_kit/eqtype/eqType_ind.con
-cic:/matita/decidable_kit/eqtype/eqType_decidable.con
-cic:/matita/decidable_kit/eqtype/eqType.ind
-cic:/matita/decidable_kit/eqtype/eqP.con
-cic:/matita/decidable_kit/eqtype/cmp_refl.con
-cic:/matita/decidable_kit/eqtype/cmpP.con
-cic:/matita/decidable_kit/eqtype/cmpC.con
-cic:/matita/decidable_kit/eqtype/cmp.con
-cic:/matita/decidable_kit/eqtype/bool_eqType.con
-cic:/matita/decidable_kit/eqtype/bool_canonical_eqType.con
-cic:/matita/decidable_kit/eqtype/bcmpP.con
-cic:/matita/decidable_kit/eqtype/bcmp.con
-cic:/matita/decidable_kit/fgraph/uniq_infgraphseq.con
-cic:/matita/decidable_kit/fgraph/setA.con
-cic:/matita/decidable_kit/fgraph/orb_refl.con
-cic:/matita/decidable_kit/fgraph/multss.con
-cic:/matita/decidable_kit/fgraph/multes.con
-cic:/matita/decidable_kit/fgraph/mkpermr.con
-cic:/matita/decidable_kit/fgraph/mem_multss.con
-cic:/matita/decidable_kit/fgraph/mem_multes.con
-cic:/matita/decidable_kit/fgraph/mem_mkpermr_size.con
-cic:/matita/decidable_kit/fgraph/mem_infgraphseq.con
-cic:/matita/decidable_kit/fgraph/mem_concat.con
-cic:/matita/decidable_kit/fgraph/iter.con
-cic:/matita/decidable_kit/fgraph/infgraphseq.con
-cic:/matita/decidable_kit/fgraph/infgraph_spec_rect.con
-cic:/matita/decidable_kit/fgraph/infgraph_spec_rec.con
-cic:/matita/decidable_kit/fgraph/infgraph_spec_inv.con
-cic:/matita/decidable_kit/fgraph/infgraph_spec_ind.con
-cic:/matita/decidable_kit/fgraph/infgraph_spec.ind
-cic:/matita/decidable_kit/fgraph/infgraphP.con
-cic:/matita/decidable_kit/fgraph/infgraph.con
-cic:/matita/decidable_kit/fgraph/fval_eqE.con
-cic:/matita/decidable_kit/fgraph/fval.con
-cic:/matita/decidable_kit/fgraph/fproof.con
-cic:/matita/decidable_kit/fgraph/fgraph_eqType.con
-cic:/matita/decidable_kit/fgraph/fgraph_eqP.con
-cic:/matita/decidable_kit/fgraph/fgraph_default.con
-cic:/matita/decidable_kit/fgraph/fgraphType_rect.con
-cic:/matita/decidable_kit/fgraph/fgraphType_rec.con
-cic:/matita/decidable_kit/fgraph/fgraphType_ind.con
-cic:/matita/decidable_kit/fgraph/fgraphType.ind
-cic:/matita/decidable_kit/fgraph/count_setA.con
-cic:/matita/decidable_kit/fintype/uniq_tail.con
-cic:/matita/decidable_kit/fintype/uniq_mem.con
-cic:/matita/decidable_kit/fintype/uniq_fintype_enum.con
-cic:/matita/decidable_kit/fintype/uniqP.con
-cic:/matita/decidable_kit/fintype/uniq.con
-cic:/matita/decidable_kit/fintype/sub_finType.con
-cic:/matita/decidable_kit/fintype/sub_enumP.con
-cic:/matita/decidable_kit/fintype/segment_finType.con
-cic:/matita/decidable_kit/fintype/segment_enum.con
-cic:/matita/decidable_kit/fintype/segment.con
-cic:/matita/decidable_kit/fintype/mem_finType.con
-cic:/matita/decidable_kit/fintype/mem_filter.con
-cic:/matita/decidable_kit/fintype/is_some.con
-cic:/matita/decidable_kit/fintype/iota_ltb.con
-cic:/matita/decidable_kit/fintype/fsort.con
-cic:/matita/decidable_kit/fintype/finType_rect.con
-cic:/matita/decidable_kit/fintype/finType_rec.con
-cic:/matita/decidable_kit/fintype/finType_ind.con
-cic:/matita/decidable_kit/fintype/finType.ind
-cic:/matita/decidable_kit/fintype/filter.con
-cic:/matita/decidable_kit/fintype/enum_uniq.con
-cic:/matita/decidable_kit/fintype/enum.con
-cic:/matita/decidable_kit/fintype/count_O_mem.con
-cic:/matita/decidable_kit/fintype/count_O.con
-cic:/matita/decidable_kit/fintype/andbC.con
-cic:/matita/decidable_kit/fintype/andbA.con
-cic:/matita/decidable_kit/fintype/Type_OF_finType.con
-cic:/matita/decidable_kit/list_aux/mem.con
-cic:/matita/decidable_kit/list_aux/list_eqType.con
-cic:/matita/decidable_kit/list_aux/lcmp_length.con
-cic:/matita/decidable_kit/list_aux/lcmpP.con
-cic:/matita/decidable_kit/list_aux/lcmp.con
-cic:/matita/decidable_kit/list_aux/count.con
-cic:/matita/decidable_kit/streicher/stepH.con
-cic:/matita/decidable_kit/streicher/step.con
-cic:/matita/decidable_kit/streicher/pirrel.con
-cic:/matita/decidable_kit/streicher/nu_k.con
-cic:/matita/decidable_kit/streicher/nu_inv.con
-cic:/matita/decidable_kit/streicher/nu.con
-cic:/matita/decidable_kit/streicher/decT.con
-cic:/matita/decidable_kit/streicher/cancel_nu_nu_inv.con
-cic:/matita/decidable_kit/streicher/cancel.con
-cic:/matita/demo/power_derivative/monomio_product.con
-cic:/matita/demo/power_derivative/monomio.con
-cic:/matita/demo/power_derivative/inj.con
-cic:/matita/demo/power_derivative/f_eq_extensional.con
-cic:/matita/demo/power_derivative/derivative_x1.con
-cic:/matita/demo/power_derivative/derivative_x0.con
-cic:/matita/demo/power_derivative/derivative_power.con
-cic:/matita/demo/power_derivative/derivative_power'.con
-cic:/matita/demo/power_derivative/derivative_mult.con
-cic:/matita/demo/power_derivative/derivative.con
-cic:/matita/demo/power_derivative/costante_sum.con
-cic:/matita/demo/power_derivative/costante.con
-cic:/matita/demo/power_derivative/Rpower.con
-cic:/matita/demo/power_derivative/Rplus_comm.con
-cic:/matita/demo/power_derivative/Rplus_assoc.con
-cic:/matita/demo/power_derivative/Rplus_Rzero_x.con
-cic:/matita/demo/power_derivative/Rplus.con
-cic:/matita/demo/power_derivative/Rmult_comm.con
-cic:/matita/demo/power_derivative/Rmult_assoc.con
-cic:/matita/demo/power_derivative/Rmult_Rzero_x.con
-cic:/matita/demo/power_derivative/Rmult_Rplus_distr.con
-cic:/matita/demo/power_derivative/Rmult_Rone_x.con
-cic:/matita/demo/power_derivative/Rmult.con
-cic:/matita/demo/power_derivative/R1.con
-cic:/matita/demo/power_derivative/R0.con
-cic:/matita/demo/power_derivative/R.con
-cic:/matita/demo/power_derivative/Fplus.con
-cic:/matita/demo/power_derivative/Fmult_zero_f.con
-cic:/matita/demo/power_derivative/Fmult_one_f.con
-cic:/matita/demo/power_derivative/Fmult_commutative.con
-cic:/matita/demo/power_derivative/Fmult_associative.con
-cic:/matita/demo/power_derivative/Fmult_Fplus_distr.con
-cic:/matita/demo/power_derivative/Fmult.con
-cic:/matita/demo/propositional_sequent_calculus/weakeningR.con
-cic:/matita/demo/propositional_sequent_calculus/transitiveb_same_atom.con
-cic:/matita/demo/propositional_sequent_calculus/transitiveb.con
-cic:/matita/demo/propositional_sequent_calculus/symmetricb_same_atom.con
-cic:/matita/demo/propositional_sequent_calculus/symmetricb_eqb.con
-cic:/matita/demo/propositional_sequent_calculus/symmetricb.con
-cic:/matita/demo/propositional_sequent_calculus/symm_orb.con
-cic:/matita/demo/propositional_sequent_calculus/symm_andb.con
-cic:/matita/demo/propositional_sequent_calculus/soundness.con
-cic:/matita/demo/propositional_sequent_calculus/sizel_0_no_axiom_is_tautology.con
-cic:/matita/demo/propositional_sequent_calculus/sizel.con
-cic:/matita/demo/propositional_sequent_calculus/size_of_sequent.con
-cic:/matita/demo/propositional_sequent_calculus/size.con
-cic:/matita/demo/propositional_sequent_calculus/sequent.con
-cic:/matita/demo/propositional_sequent_calculus/same_atom_to_exists.con
-cic:/matita/demo/propositional_sequent_calculus/same_atom_to_eq.con
-cic:/matita/demo/propositional_sequent_calculus/same_atom.con
-cic:/matita/demo/propositional_sequent_calculus/orb_not_b_b.con
-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
-cic:/matita/demo/propositional_sequent_calculus/mem_to_exists_l1_l2.con
-cic:/matita/demo/propositional_sequent_calculus/mem_same_atom_to_exists.con
-cic:/matita/demo/propositional_sequent_calculus/look_for_axiom.con
-cic:/matita/demo/propositional_sequent_calculus/is_tautology.con
-cic:/matita/demo/propositional_sequent_calculus/interp.con
-cic:/matita/demo/propositional_sequent_calculus/formula_of_sequent.con
-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:/CoRN/algebra/Basics/well_founded_ltof.con
+cic:/CoRN/algebra/Basics/well_founded_induction_type.con
+cic:/CoRN/algebra/Basics/well_founded.con
+cic:/CoRN/algebra/Basics/surj_not.con
+cic:/CoRN/algebra/Basics/surj_lt_subproof.con
+cic:/CoRN/algebra/Basics/surj_lt.con
+cic:/CoRN/algebra/Basics/surj_le_subproof.con
+cic:/CoRN/algebra/Basics/surj_le.con
+cic:/CoRN/algebra/Basics/surj_eq_subproof.con
+cic:/CoRN/algebra/Basics/surj_eq.con
+cic:/CoRN/algebra/Basics/proper_caseZ_diff_subproof0.con
+cic:/CoRN/algebra/Basics/proper_caseZ_diff_subproof.con
+cic:/CoRN/algebra/Basics/proper_caseZ_diff.con
+cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con
+cic:/CoRN/algebra/Basics/power.con
+cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con
+cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con
+cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con
+cic:/CoRN/algebra/Basics/nats_Z_ind.con
+cic:/CoRN/algebra/Basics/nat_fac_gtzero.con
+cic:/CoRN/algebra/Basics/minus4_subproof1.con
+cic:/CoRN/algebra/Basics/minus4_subproof0.con
+cic:/CoRN/algebra/Basics/minus4_subproof.con
+cic:/CoRN/algebra/Basics/minus4.con
+cic:/CoRN/algebra/Basics/minus3_subproof1.con
+cic:/CoRN/algebra/Basics/minus3_subproof0.con
+cic:/CoRN/algebra/Basics/minus3_subproof.con
+cic:/CoRN/algebra/Basics/minus3.con
+cic:/CoRN/algebra/Basics/min_convert_is_NEG.con
+cic:/CoRN/algebra/Basics/ltof.con
+cic:/CoRN/algebra/Basics/lt_z_two.con
+cic:/CoRN/algebra/Basics/lt_wf_rect.con
+cic:/CoRN/algebra/Basics/lt_mult_right.con
+cic:/CoRN/algebra/Basics/lt_lt_minus_subproof.con
+cic:/CoRN/algebra/Basics/lt_lt_minus.con
+cic:/CoRN/algebra/Basics/lt_le_dec.con
+cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con
+cic:/CoRN/algebra/Basics/le_pred.con
+cic:/CoRN/algebra/Basics/le_mult_right.con
+cic:/CoRN/algebra/Basics/inject_nat_convert.con
+cic:/CoRN/algebra/Basics/induction_ltof2T.con
+cic:/CoRN/algebra/Basics/fac.con
+cic:/CoRN/algebra/Basics/diff_Z_ind_subproof.con
+cic:/CoRN/algebra/Basics/diff_Z_ind.con
+cic:/CoRN/algebra/Basics/convert_is_POS.con
+cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con
+cic:/CoRN/algebra/Basics/caseZ_diff_O.con
+cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con
+cic:/CoRN/algebra/Basics/caseZ_diff.con
+cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con
+cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con
+cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con
+cic:/CoRN/algebra/Basics/Zmult_absorb.con
+cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con
+cic:/CoRN/algebra/Basics/Zlt_opp.con
+cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con
+cic:/CoRN/algebra/Basics/Zgt_not_eq.con
+cic:/CoRN/algebra/Basics/Z_to_nat_correct.con
+cic:/CoRN/algebra/Basics/Z_to_nat.con
+cic:/CoRN/algebra/Basics/Z_exh.con
+cic:/CoRN/algebra/Basics/POS_anti_convert.con
+cic:/CoRN/algebra/Basics/NEG_anti_convert.con
+cic:/CoRN/algebra/Basics/Acc_iter.con
+cic:/CoRN/algebra/Basics/Acc_inv.con
+cic:/CoRN/algebra/Basics/Acc_ind.con
+cic:/CoRN/algebra/Basics/Acc.ind
+cic:/CoRN/algebra/CAbGroups/zmult_zero.con
+cic:/CoRN/algebra/CAbGroups/zmult_wd.con
+cic:/CoRN/algebra/CAbGroups/zmult_plus.con
+cic:/CoRN/algebra/CAbGroups/zmult_plus'.con
+cic:/CoRN/algebra/CAbGroups/zmult_one.con
+cic:/CoRN/algebra/CAbGroups/zmult_mult.con
+cic:/CoRN/algebra/CAbGroups/zmult_min_one.con
+cic:/CoRN/algebra/CAbGroups/zmult_char_subproof1.con
+cic:/CoRN/algebra/CAbGroups/zmult_char_subproof0.con
+cic:/CoRN/algebra/CAbGroups/zmult_char_subproof.con
+cic:/CoRN/algebra/CAbGroups/zmult_char.con
+cic:/CoRN/algebra/CAbGroups/zmult_Zero.con
+cic:/CoRN/algebra/CAbGroups/zmult.con
+cic:/CoRN/algebra/CAbGroups/plus_runit.con
+cic:/CoRN/algebra/CAbGroups/plus_rext.con
+cic:/CoRN/algebra/CAbGroups/plus_is_fun.con
+cic:/CoRN/algebra/CAbGroups/plus_fun.con
+cic:/CoRN/algebra/CAbGroups/plus_cancel_ap_lft.con
+cic:/CoRN/algebra/CAbGroups/op_lft_resp_ap.con
+cic:/CoRN/algebra/CAbGroups/nmult_wd.con
+cic:/CoRN/algebra/CAbGroups/nmult_plus.con
+cic:/CoRN/algebra/CAbGroups/nmult_plus'.con
+cic:/CoRN/algebra/CAbGroups/nmult_one.con
+cic:/CoRN/algebra/CAbGroups/nmult_mult.con
+cic:/CoRN/algebra/CAbGroups/nmult_inv.con
+cic:/CoRN/algebra/CAbGroups/nmult_Zero.con
+cic:/CoRN/algebra/CAbGroups/nmult.con
+cic:/CoRN/algebra/CAbGroups/minus_plus.con
+cic:/CoRN/algebra/CAbGroups/isabgrp_scrr.con
+cic:/CoRN/algebra/CAbGroups/is_CAbGroup.con
+cic:/CoRN/algebra/CAbGroups/inv_inv'.con
+cic:/CoRN/algebra/CAbGroups/cag_proof.con
+cic:/CoRN/algebra/CAbGroups/cag_op_inv.con
+cic:/CoRN/algebra/CAbGroups/cag_crr.con
+cic:/CoRN/algebra/CAbGroups/cag_commutes_unfolded.con
+cic:/CoRN/algebra/CAbGroups/cag_commutes.con
+cic:/CoRN/algebra/CAbGroups/cag_ap_cancel_lft.con
+cic:/CoRN/algebra/CAbGroups/assoc_1.con
+cic:/CoRN/algebra/CAbGroups/CAbGroup_rect.con
+cic:/CoRN/algebra/CAbGroups/CAbGroup_rec.con
+cic:/CoRN/algebra/CAbGroups/CAbGroup_is_CAbGroup.con
+cic:/CoRN/algebra/CAbGroups/CAbGroup_ind.con
+cic:/CoRN/algebra/CAbGroups/CAbGroup.ind
+cic:/CoRN/algebra/CAbGroups/Build_SubCAbGroup.con
+cic:/CoRN/algebra/CAbGroups/Build_CSemiGroup'.con
+cic:/CoRN/algebra/CAbGroups/Build_CMonoid'.con
+cic:/CoRN/algebra/CAbGroups/Build_CGroup'.con
+cic:/CoRN/algebra/CAbGroups/Build_CAbGroup'.con
+cic:/CoRN/algebra/CAbMonoids/isabgrp_scrr.con
+cic:/CoRN/algebra/CAbMonoids/is_CAbMonoid.con
+cic:/CoRN/algebra/CAbMonoids/cam_proof.con
+cic:/CoRN/algebra/CAbMonoids/cam_crr.con
+cic:/CoRN/algebra/CAbMonoids/cam_commutes_unfolded.con
+cic:/CoRN/algebra/CAbMonoids/cam_commutes.con
+cic:/CoRN/algebra/CAbMonoids/CAbMonoid_rect.con
+cic:/CoRN/algebra/CAbMonoids/CAbMonoid_rec.con
+cic:/CoRN/algebra/CAbMonoids/CAbMonoid_is_CAbMonoid.con
+cic:/CoRN/algebra/CAbMonoids/CAbMonoid_ind.con
+cic:/CoRN/algebra/CAbMonoids/CAbMonoid.ind
+cic:/CoRN/algebra/CAbMonoids/Build_SubCAbMonoid.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/tau_surj.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/tau_strext.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/tau_is_fun.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/tau.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/sigst_strext.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/sigst_is_fun.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/sigst_inj.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/sigst.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/cswdpredR.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/cswdpred.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/cspredR.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/cspred.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/cs_is_comod.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/cs_is_coideal.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/cs_as_comod.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/cs_as_coideal.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau_surj.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau_strext.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau_is_fun.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst_strext.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst_is_fun.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst_inj.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/RingHomTheorem.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/RdivCsR.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/ModHomTheorem.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/CsR.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/Cs.con
+cic:/CoRN/algebra/CHomomorphism_Theorems/AdivCs.con
+cic:/CoRN/algebra/CIdeals/is_ideal_rect.con
+cic:/CoRN/algebra/CIdeals/is_ideal_rec.con
+cic:/CoRN/algebra/CIdeals/is_ideal_ind.con
+cic:/CoRN/algebra/CIdeals/is_ideal.ind
+cic:/CoRN/algebra/CIdeals/is_coideal_rect.con
+cic:/CoRN/algebra/CIdeals/is_coideal_rec.con
+cic:/CoRN/algebra/CIdeals/is_coideal_ind.con
+cic:/CoRN/algebra/CIdeals/is_coideal.ind
+cic:/CoRN/algebra/CIdeals/idprpl.con
+cic:/CoRN/algebra/CIdeals/idproof.con
+cic:/CoRN/algebra/CIdeals/idpred.con
+cic:/CoRN/algebra/CIdeals/ideal_rect.con
+cic:/CoRN/algebra/CIdeals/ideal_rec.con
+cic:/CoRN/algebra/CIdeals/ideal_is_ideal.con
+cic:/CoRN/algebra/CIdeals/ideal_ind.con
+cic:/CoRN/algebra/CIdeals/ideal_as_CSetoid.con
+cic:/CoRN/algebra/CIdeals/ideal.ind
+cic:/CoRN/algebra/CIdeals/idax.con
+cic:/CoRN/algebra/CIdeals/coideal_wd.con
+cic:/CoRN/algebra/CIdeals/coideal_rect.con
+cic:/CoRN/algebra/CIdeals/coideal_rec.con
+cic:/CoRN/algebra/CIdeals/coideal_plus.con
+cic:/CoRN/algebra/CIdeals/coideal_nonzero.con
+cic:/CoRN/algebra/CIdeals/coideal_nontriv.con
+cic:/CoRN/algebra/CIdeals/coideal_mult.con
+cic:/CoRN/algebra/CIdeals/coideal_is_coideal.con
+cic:/CoRN/algebra/CIdeals/coideal_ind.con
+cic:/CoRN/algebra/CIdeals/coideal_as_CSetoid.con
+cic:/CoRN/algebra/CIdeals/coideal_apzero.con
+cic:/CoRN/algebra/CIdeals/coideal.ind
+cic:/CoRN/algebra/CIdeals/ciproof.con
+cic:/CoRN/algebra/CIdeals/cipred.con
+cic:/CoRN/algebra/CIdeals/ciplus.con
+cic:/CoRN/algebra/CIdeals/cinontriv.con
+cic:/CoRN/algebra/CIdeals/cimult.con
+cic:/CoRN/algebra/CIdeals/ciapzero.con
+cic:/CoRN/algebra/CLogic/weird_mon_covers.con
+cic:/CoRN/algebra/CLogic/to_Codd_even.con
+cic:/CoRN/algebra/CLogic/to_Codd.con
+cic:/CoRN/algebra/CLogic/to_Ceven.con
+cic:/CoRN/algebra/CLogic/toCle.con
+cic:/CoRN/algebra/CLogic/toCProp_rect.con
+cic:/CoRN/algebra/CLogic/toCProp_rec.con
+cic:/CoRN/algebra/CLogic/toCProp_lt.con
+cic:/CoRN/algebra/CLogic/toCProp_ind.con
+cic:/CoRN/algebra/CLogic/toCProp_e.con
+cic:/CoRN/algebra/CLogic/toCProp_Zlt.con
+cic:/CoRN/algebra/CLogic/toCProp.ind
+cic:/CoRN/algebra/CLogic/str_finite_or_elim.con
+cic:/CoRN/algebra/CLogic/sig2T_rect.con
+cic:/CoRN/algebra/CLogic/sig2T_rec.con
+cic:/CoRN/algebra/CLogic/sig2T_ind.con
+cic:/CoRN/algebra/CLogic/sig2T.ind
+cic:/CoRN/algebra/CLogic/proj2b_sig2T.con
+cic:/CoRN/algebra/CLogic/proj2a_sig2T.con
+cic:/CoRN/algebra/CLogic/proj2_sigT.con
+cic:/CoRN/algebra/CLogic/proj1_sigT.con
+cic:/CoRN/algebra/CLogic/proj1_sig2T.con
+cic:/CoRN/algebra/CLogic/pred_lt.con
+cic:/CoRN/algebra/CLogic/plus_pred_pred_plus.con
+cic:/CoRN/algebra/CLogic/plus_eq_one_imp_eq_zero.con
+cic:/CoRN/algebra/CLogic/odd_induction.con
+cic:/CoRN/algebra/CLogic/odd_ind.con
+cic:/CoRN/algebra/CLogic/odd_double_ind.con
+cic:/CoRN/algebra/CLogic/not_r_sum_rec.con
+cic:/CoRN/algebra/CLogic/not_r_cor_rect.con
+cic:/CoRN/algebra/CLogic/not_not_lt.con
+cic:/CoRN/algebra/CLogic/not_l_sum_rec.con
+cic:/CoRN/algebra/CLogic/not_l_cor_rect.con
+cic:/CoRN/algebra/CLogic/nat_nat_pos.con
+cic:/CoRN/algebra/CLogic/nat_mon_imp_mon'.con
+cic:/CoRN/algebra/CLogic/nat_mon_imp_inj.con
+cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon_le.con
+cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon.con
+cic:/CoRN/algebra/CLogic/nat_less_n_pred.con
+cic:/CoRN/algebra/CLogic/nat_less_n_pred'.con
+cic:/CoRN/algebra/CLogic/nat_complete_double_induction.con
+cic:/CoRN/algebra/CLogic/nat_complete_double_ind.con
+cic:/CoRN/algebra/CLogic/my_Cle_ind.con
+cic:/CoRN/algebra/CLogic/mon_fun_covers.con
+cic:/CoRN/algebra/CLogic/member_app.con
+cic:/CoRN/algebra/CLogic/member.con
+cic:/CoRN/algebra/CLogic/lt_pred'.con
+cic:/CoRN/algebra/CLogic/lt_8.con
+cic:/CoRN/algebra/CLogic/lt_5.con
+cic:/CoRN/algebra/CLogic/lt_10.con
+cic:/CoRN/algebra/CLogic/le_2.con
+cic:/CoRN/algebra/CLogic/le_1.con
+cic:/CoRN/algebra/CLogic/kseq_prop.con
+cic:/CoRN/algebra/CLogic/four_induction.con
+cic:/CoRN/algebra/CLogic/four_ind.con
+cic:/CoRN/algebra/CLogic/finite_or_elim.con
+cic:/CoRN/algebra/CLogic/even_plus_n_n.con
+cic:/CoRN/algebra/CLogic/even_or_odd_plus_gt.con
+cic:/CoRN/algebra/CLogic/even_or_odd_plus.con
+cic:/CoRN/algebra/CLogic/even_induction.con
+cic:/CoRN/algebra/CLogic/even_ind.con
+cic:/CoRN/algebra/CLogic/choice.con
+cic:/CoRN/algebra/CLogic/absolu_2.con
+cic:/CoRN/algebra/CLogic/absolu_1.con
+cic:/CoRN/algebra/CLogic/Zsgn_5.con
+cic:/CoRN/algebra/CLogic/Zsgn_4.con
+cic:/CoRN/algebra/CLogic/Zsgn_3.con
+cic:/CoRN/algebra/CLogic/Zsgn_2.con
+cic:/CoRN/algebra/CLogic/Zsgn_1.con
+cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con
+cic:/CoRN/algebra/CLogic/Zlts.con
+cic:/CoRN/algebra/CLogic/Zgt_mult_reg_absorb_l.con
+cic:/CoRN/algebra/CLogic/Zgt_mult_conv_absorb_l.con
+cic:/CoRN/algebra/CLogic/ZL9.con
+cic:/CoRN/algebra/CLogic/ZL4'.con
+cic:/CoRN/algebra/CLogic/Ttransitive.con
+cic:/CoRN/algebra/CLogic/Tsymmetric.con
+cic:/CoRN/algebra/CLogic/Trelation.con
+cic:/CoRN/algebra/CLogic/Treflexive.con
+cic:/CoRN/algebra/CLogic/Tequiv.con
+cic:/CoRN/algebra/CLogic/S_predn.con
+cic:/CoRN/algebra/CLogic/Not.con
+cic:/CoRN/algebra/CLogic/Iff_trans.con
+cic:/CoRN/algebra/CLogic/Iff_sym.con
+cic:/CoRN/algebra/CLogic/Iff_right.con
+cic:/CoRN/algebra/CLogic/Iff_refl.con
+cic:/CoRN/algebra/CLogic/Iff_left.con
+cic:/CoRN/algebra/CLogic/Iff_imp_imp.con
+cic:/CoRN/algebra/CLogic/Iff.con
+cic:/CoRN/algebra/CLogic/Ctransitive.con
+cic:/CoRN/algebra/CLogic/Csymmetric.con
+cic:/CoRN/algebra/CLogic/Crelation.con
+cic:/CoRN/algebra/CLogic/Creflexive.con
+cic:/CoRN/algebra/CLogic/Cpred_succ_Z_ind.con
+cic:/CoRN/algebra/CLogic/Codd_to.con
+cic:/CoRN/algebra/CLogic/Codd_rect.con
+cic:/CoRN/algebra/CLogic/Codd_rec.con
+cic:/CoRN/algebra/CLogic/Codd_ind.con
+cic:/CoRN/algebra/CLogic/Codd_even_to.con
+cic:/CoRN/algebra/CLogic/Codd.ind
+cic:/CoRN/algebra/CLogic/Cnats_Z_ind.con
+cic:/CoRN/algebra/CLogic/Cnat_total_order.con
+cic:/CoRN/algebra/CLogic/Cnat_double_ind.con
+cic:/CoRN/algebra/CLogic/Clt_to.con
+cic:/CoRN/algebra/CLogic/Clt_le_weak.con
+cic:/CoRN/algebra/CLogic/Clt.con
+cic:/CoRN/algebra/CLogic/Cle_to.con
+cic:/CoRN/algebra/CLogic/Cle_rect.con
+cic:/CoRN/algebra/CLogic/Cle_rec.con
+cic:/CoRN/algebra/CLogic/Cle_n_S.con
+cic:/CoRN/algebra/CLogic/Cle_le_S_eq.con
+cic:/CoRN/algebra/CLogic/Cle_ind.con
+cic:/CoRN/algebra/CLogic/Cle.ind
+cic:/CoRN/algebra/CLogic/Ceven_to.con
+cic:/CoRN/algebra/CLogic/Ceven_rect.con
+cic:/CoRN/algebra/CLogic/Ceven_rec.con
+cic:/CoRN/algebra/CLogic/Ceven_ind.con
+cic:/CoRN/algebra/CLogic/Cequiv.con
+cic:/CoRN/algebra/CLogic/Cdiff_Z_ind_subproof.con
+cic:/CoRN/algebra/CLogic/Cdiff_Z_ind.con
+cic:/CoRN/algebra/CLogic/Cdecidable.con
+cic:/CoRN/algebra/CLogic/CdeMorgan_ex_all.con
+cic:/CoRN/algebra/CLogic/Ccontrapos'.con
+cic:/CoRN/algebra/CLogic/CZlt_to.con
+cic:/CoRN/algebra/CLogic/CZ_exh.con
+cic:/CoRN/algebra/CLogic/CTrue_rect.con
+cic:/CoRN/algebra/CLogic/CTrue_rec.con
+cic:/CoRN/algebra/CLogic/CTrue_ind.con
+cic:/CoRN/algebra/CLogic/CTrue.ind
+cic:/CoRN/algebra/CLogic/CProp.con
+cic:/CoRN/algebra/CLogic/COr_rect.con
+cic:/CoRN/algebra/CLogic/COr_rec.con
+cic:/CoRN/algebra/CLogic/COr_ind.con
+cic:/CoRN/algebra/CLogic/COr.ind
+cic:/CoRN/algebra/CLogic/CNot_Not_or.con
+cic:/CoRN/algebra/CLogic/CNot.con
+cic:/CoRN/algebra/CLogic/CFalse_rect.con
+cic:/CoRN/algebra/CLogic/CFalse_rec.con
+cic:/CoRN/algebra/CLogic/CFalse_ind.con
+cic:/CoRN/algebra/CLogic/CFalse.ind
+cic:/CoRN/algebra/CLogic/CAnd_rect.con
+cic:/CoRN/algebra/CLogic/CAnd_rec.con
+cic:/CoRN/algebra/CLogic/CAnd_proj2.con
+cic:/CoRN/algebra/CLogic/CAnd_proj1.con
+cic:/CoRN/algebra/CLogic/CAnd_ind.con
+cic:/CoRN/algebra/CLogic/CAnd.ind
+cic:/CoRN/algebra/CModule_Homomorphisms/mh_strext.con
+cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_zero.con
+cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_unit.con
+cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_plus.con
+cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_mult.con
+cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_minus.con
+cic:/CoRN/algebra/CModule_Homomorphisms/mh_apzero.con
+cic:/CoRN/algebra/CModule_Homomorphisms/hommap.con
+cic:/CoRN/algebra/CModule_Homomorphisms/hom3.con
+cic:/CoRN/algebra/CModule_Homomorphisms/hom2.con
+cic:/CoRN/algebra/CModule_Homomorphisms/hom1.con
+cic:/CoRN/algebra/CModule_Homomorphisms/fun_pres_unit.con
+cic:/CoRN/algebra/CModule_Homomorphisms/fun_pres_plus.con
+cic:/CoRN/algebra/CModule_Homomorphisms/fun_pres_mult.con
+cic:/CoRN/algebra/CModule_Homomorphisms/ModHom_rect.con
+cic:/CoRN/algebra/CModule_Homomorphisms/ModHom_rec.con
+cic:/CoRN/algebra/CModule_Homomorphisms/ModHom_ind.con
+cic:/CoRN/algebra/CModule_Homomorphisms/ModHom.ind
+cic:/CoRN/algebra/CModules/submod_rect.con
+cic:/CoRN/algebra/CModules/submod_rec.con
+cic:/CoRN/algebra/CModules/submod_is_submod.con
+cic:/CoRN/algebra/CModules/submod_ind.con
+cic:/CoRN/algebra/CModules/submod_as_CSetoid.con
+cic:/CoRN/algebra/CModules/submod.ind
+cic:/CoRN/algebra/CModules/smzero.con
+cic:/CoRN/algebra/CModules/smproof.con
+cic:/CoRN/algebra/CModules/smpred.con
+cic:/CoRN/algebra/CModules/smplus.con
+cic:/CoRN/algebra/CModules/smmult.con
+cic:/CoRN/algebra/CModules/rm_proof.con
+cic:/CoRN/algebra/CModules/rm_pl2.con
+cic:/CoRN/algebra/CModules/rm_pl1.con
+cic:/CoRN/algebra/CModules/rm_one.con
+cic:/CoRN/algebra/CModules/rm_mult.con
+cic:/CoRN/algebra/CModules/rm_mu.con
+cic:/CoRN/algebra/CModules/rm_crr.con
+cic:/CoRN/algebra/CModules/mu_zerox.con
+cic:/CoRN/algebra/CModules/mu_strext.con
+cic:/CoRN/algebra/CModules/mu_plus2.con
+cic:/CoRN/algebra/CModules/mu_plus1.con
+cic:/CoRN/algebra/CModules/mu_one.con
+cic:/CoRN/algebra/CModules/mu_mult.con
+cic:/CoRN/algebra/CModules/mu_minusonex.con
+cic:/CoRN/algebra/CModules/mu_minusax.con
+cic:/CoRN/algebra/CModules/mu_azero.con
+cic:/CoRN/algebra/CModules/mu_axap0_xap0.con
+cic:/CoRN/algebra/CModules/mu_axap0_aap0.con
+cic:/CoRN/algebra/CModules/mu_aminusx.con
+cic:/CoRN/algebra/CModules/mu0help2.con
+cic:/CoRN/algebra/CModules/mu0help.con
+cic:/CoRN/algebra/CModules/is_submod_rect.con
+cic:/CoRN/algebra/CModules/is_submod_rec.con
+cic:/CoRN/algebra/CModules/is_submod_ind.con
+cic:/CoRN/algebra/CModules/is_submod.ind
+cic:/CoRN/algebra/CModules/is_comod_rect.con
+cic:/CoRN/algebra/CModules/is_comod_rec.con
+cic:/CoRN/algebra/CModules/is_comod_ind.con
+cic:/CoRN/algebra/CModules/is_comod.ind
+cic:/CoRN/algebra/CModules/is_RModule_rect.con
+cic:/CoRN/algebra/CModules/is_RModule_rec.con
+cic:/CoRN/algebra/CModules/is_RModule_ind.con
+cic:/CoRN/algebra/CModules/is_RModule.ind
+cic:/CoRN/algebra/CModules/comod_wd.con
+cic:/CoRN/algebra/CModules/comod_rect.con
+cic:/CoRN/algebra/CModules/comod_rec.con
+cic:/CoRN/algebra/CModules/comod_plus.con
+cic:/CoRN/algebra/CModules/comod_nonzero.con
+cic:/CoRN/algebra/CModules/comod_mult.con
+cic:/CoRN/algebra/CModules/comod_is_comod.con
+cic:/CoRN/algebra/CModules/comod_ind.con
+cic:/CoRN/algebra/CModules/comod_as_CSetoid.con
+cic:/CoRN/algebra/CModules/comod_apzero.con
+cic:/CoRN/algebra/CModules/comod.ind
+cic:/CoRN/algebra/CModules/cmproof.con
+cic:/CoRN/algebra/CModules/cmpred.con
+cic:/CoRN/algebra/CModules/cmplus.con
+cic:/CoRN/algebra/CModules/cmmult.con
+cic:/CoRN/algebra/CModules/cmapzero.con
+cic:/CoRN/algebra/CModules/R_is_RModule.con
+cic:/CoRN/algebra/CModules/R_as_RModule.con
+cic:/CoRN/algebra/CModules/RModule_rect.con
+cic:/CoRN/algebra/CModules/RModule_rec.con
+cic:/CoRN/algebra/CModules/RModule_is_RModule.con
+cic:/CoRN/algebra/CModules/RModule_ind.con
+cic:/CoRN/algebra/CModules/RModule.ind
+cic:/matita/dama/bishop_set/le_le_eq.con
+cic:/matita/dama/bishop_set/le_antisymmetric.con
+cic:/matita/dama/bishop_set/eq_trans_.con
+cic:/matita/dama/bishop_set/eq_sym_.con
+cic:/matita/dama/bishop_set/eq_sym.con
+cic:/matita/dama/bishop_set/eq_reflexive.con
+cic:/matita/dama/bishop_set/eq.con
+cic:/matita/dama/bishop_set/bs_symmetric.con
+cic:/matita/dama/bishop_set/bs_cotransitive.con
+cic:/matita/dama/bishop_set/bs_coreflexive.con
+cic:/matita/dama/bishop_set/bs_carr.con
+cic:/matita/dama/bishop_set/bs_apart.con
+cic:/matita/dama/bishop_set/bishop_set_rect.con
+cic:/matita/dama/bishop_set/bishop_set_rec.con
+cic:/matita/dama/bishop_set/bishop_set_of_ordered_set.con
+cic:/matita/dama/bishop_set/bishop_set_ind.con
+cic:/matita/dama/bishop_set/bishop_set.ind
+cic:/matita/dama/bishop_set_rewrite/le_rewr.con
+cic:/matita/dama/bishop_set_rewrite/le_rewl.con
+cic:/matita/dama/bishop_set_rewrite/exc_rewr.con
+cic:/matita/dama/bishop_set_rewrite/exc_rewl.con
+cic:/matita/dama/bishop_set_rewrite/eq_trans.con
+cic:/matita/dama/bishop_set_rewrite/ap_rewr.con
+cic:/matita/dama/bishop_set_rewrite/ap_rewl.con
+cic:/matita/dama/cprop_connectives/transitive.con
+cic:/matita/dama/cprop_connectives/symmetric.con
+cic:/matita/dama/cprop_connectives/reflexive.con
+cic:/matita/dama/cprop_connectives/exT_rect.con
+cic:/matita/dama/cprop_connectives/exT_rec.con
+cic:/matita/dama/cprop_connectives/exT_ind.con
+cic:/matita/dama/cprop_connectives/exT.ind
+cic:/matita/dama/cprop_connectives/cotransitive.con
+cic:/matita/dama/cprop_connectives/coreflexive.con
+cic:/matita/dama/cprop_connectives/antisymmetric.con
+cic:/matita/dama/cprop_connectives/Or_rect.con
+cic:/matita/dama/cprop_connectives/Or_rec.con
+cic:/matita/dama/cprop_connectives/Or_ind.con
+cic:/matita/dama/cprop_connectives/Or.ind
+cic:/matita/dama/cprop_connectives/Not.con
+cic:/matita/dama/cprop_connectives/False_rect.con
+cic:/matita/dama/cprop_connectives/False_rec.con
+cic:/matita/dama/cprop_connectives/False_ind.con
+cic:/matita/dama/cprop_connectives/False.ind
+cic:/matita/dama/cprop_connectives/And_rect.con
+cic:/matita/dama/cprop_connectives/And_rec.con
+cic:/matita/dama/cprop_connectives/And_ind.con
+cic:/matita/dama/cprop_connectives/And.ind
+cic:/matita/dama/ordered_set/os_excess.con
+cic:/matita/dama/ordered_set/os_cotransitive.con
+cic:/matita/dama/ordered_set/os_coreflexive.con
+cic:/matita/dama/ordered_set/os_carr.con
+cic:/matita/dama/ordered_set/ordered_set_rect.con
+cic:/matita/dama/ordered_set/ordered_set_rec.con
+cic:/matita/dama/ordered_set/ordered_set_ind.con
+cic:/matita/dama/ordered_set/ordered_set.ind
+cic:/matita/dama/ordered_set/le_transitive.con
+cic:/matita/dama/ordered_set/le_reflexive.con
+cic:/matita/dama/ordered_set/le.con
+cic:/matita/dama/ordered_set/exc_le_variance.con
+cic:/matita/dama/sequence/sequence.con
+cic:/matita/dama/sequence/fun_of_sequence.con
+cic:/matita/dama/supremum/upper_bound.con
+cic:/matita/dama/supremum/uniq_supremum.con
+cic:/matita/dama/supremum/strong_sup.con
+cic:/matita/dama/supremum/increasing.con