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
cic:/matita/higher_order_defs/functions/symmetric2.con
cic:/matita/higher_order_defs/functions/symmetric.con
cic:/matita/higher_order_defs/functions/surjective.con
cic:/matita/higher_order_defs/functions/monotonic.con
cic:/matita/higher_order_defs/functions/injective.con
cic:/matita/higher_order_defs/functions/eq_f_g_h.con
cic:/matita/higher_order_defs/functions/distributive2.con
cic:/matita/higher_order_defs/functions/distributive.con
cic:/matita/higher_order_defs/functions/compose.con
cic:/matita/higher_order_defs/functions/associative.con
cic:/matita/higher_order_defs/relations/transitive.con
cic:/matita/higher_order_defs/relations/tight_apart.con
cic:/matita/higher_order_defs/relations/symmetric.con
cic:/matita/higher_order_defs/relations/relation.con
cic:/matita/higher_order_defs/relations/reflexive.con
cic:/matita/higher_order_defs/relations/irreflexive.con
cic:/matita/higher_order_defs/relations/cotransitive.con
cic:/matita/higher_order_defs/relations/antisymmetric.con
cic:/matita/logic/connectives/proj2.con
cic:/matita/logic/connectives/proj1.con
cic:/matita/logic/connectives/iff.con
cic:/matita/logic/connectives/ex_ind.con
cic:/matita/logic/connectives/ex2_ind.con
cic:/matita/logic/connectives/ex2.ind
cic:/matita/logic/connectives/ex.ind
cic:/matita/logic/connectives/decidable.con
cic:/matita/logic/connectives/absurd.con
cic:/matita/logic/connectives/True_rect.con
cic:/matita/logic/connectives/True_rec.con
cic:/matita/logic/connectives/True_ind.con
cic:/matita/logic/connectives/True.ind
cic:/matita/logic/connectives/Or_ind.con
cic:/matita/logic/connectives/Or_ind'.con
cic:/matita/logic/connectives/Or.ind
cic:/matita/logic/connectives/Not.con
cic:/matita/logic/connectives/False_rect.con
cic:/matita/logic/connectives/False_rec.con
cic:/matita/logic/connectives/False_ind.con
cic:/matita/logic/connectives/False.ind
cic:/matita/logic/connectives/And_rect.con
cic:/matita/logic/connectives/And_rec.con
cic:/matita/logic/connectives/And_ind.con
cic:/matita/logic/connectives/And.ind
cic:/matita/logic/equality/transitive_eq.con
cic:/matita/logic/equality/trans_sym_eq.con
cic:/matita/logic/equality/trans_eq.con
cic:/matita/logic/equality/symmetric_eq.con
cic:/matita/logic/equality/sym_eq.con
cic:/matita/logic/equality/reflexive_eq.con
cic:/matita/logic/equality/nu_left_inv.con
cic:/matita/logic/equality/nu_inv.con
cic:/matita/logic/equality/nu_constant.con
cic:/matita/logic/equality/nu.con
cic:/matita/logic/equality/eq_to_eq_to_eq_p_q.con
cic:/matita/logic/equality/eq_rect.con
cic:/matita/logic/equality/eq_rect'.con
cic:/matita/logic/equality/eq_rec.con
cic:/matita/logic/equality/eq_ind.con
cic:/matita/logic/equality/eq_f2.con
cic:/matita/logic/equality/eq_f.con
cic:/matita/logic/equality/eq_f'.con
cic:/matita/logic/equality/eq_elim_r.con
cic:/matita/logic/equality/eq_elim_r'.con
cic:/matita/logic/equality/eq_elim_r''.con
cic:/matita/logic/equality/eq_OF_eq2.con
cic:/matita/logic/equality/eq_OF_eq1.con
cic:/matita/logic/equality/eq_OF_eq.con
cic:/matita/logic/equality/eq.ind
cic:/matita/logic/equality/comp.con
cic:/matita/nat/nat/pred_Sn.con
cic:/matita/nat/nat/pred.con
cic:/matita/nat/nat/not_zero.con
cic:/matita/nat/nat/not_eq_n_Sn.con
cic:/matita/nat/nat/not_eq_S.con
cic:/matita/nat/nat/not_eq_O_S.con
cic:/matita/nat/nat/nat_rect.con
cic:/matita/nat/nat/nat_rec.con
cic:/matita/nat/nat/nat_ind.con
cic:/matita/nat/nat/nat_elim2.con
cic:/matita/nat/nat/nat_case1.con
cic:/matita/nat/nat/nat_case.con
cic:/matita/nat/nat/nat.ind
cic:/matita/nat/nat/injective_S.con
cic:/matita/nat/nat/inj_S.con
cic:/matita/nat/nat/decidable_eq_nat.con