-cic:/matita/nat/neper/sigma_p_log_div2.con
-cic:/matita/nat/neper/sigma_p_log_div1.con
-cic:/matita/nat/neper/sigma_p_log_div.con
-cic:/matita/nat/neper/sigma_p_div_exp.con
-cic:/matita/nat/neper/neper_sigma_p3.con
-cic:/matita/nat/neper/neper_sigma_p2.con
-cic:/matita/nat/neper/neper_sigma_p1.con
-cic:/matita/nat/neper/neper_monotonic.con
-cic:/matita/nat/neper/lt_exp_sigma_p_exp.con
-cic:/matita/nat/neper/lt_exp_Sn_n_SSSO.con
-cic:/matita/nat/neper/lt_exp_Sn_m_SSSO.con
-cic:/matita/nat/neper/lt_SO_to_lt_exp_Sn_n_SSSO.con
-cic:/matita/nat/neper/le_sigma_p_div_log_div_pred_log.con
-cic:/matita/nat/neper/le_log_exp_fact_sigma_p.con
-cic:/matita/nat/neper/le_log_exp_Sn_log_exp_n.con
-cic:/matita/nat/neper/le_log_div_sigma_p.con
-cic:/matita/nat/neper/le_fact_exp1.con
-cic:/matita/nat/neper/le_fact_exp.con
-cic:/matita/nat/neper/le_exp_sigma_p_exp.con
-cic:/matita/nat/neper/le_exp_div.con
-cic:/matita/nat/neper/le_exp_SSO_fact.con
-cic:/matita/nat/neper/le_SSO_neper.con
-cic:/matita/nat/neper/le_SSO_exp_neper.con
-cic:/matita/nat/neper/eq_fact_pi_p.con
-cic:/matita/nat/neper/eq_exp_pi_p.con
-cic:/matita/nat/neper/divides_times_to_eq.con
-cic:/matita/nat/neper/divides_times_to_divides_div.con
-cic:/matita/nat/neper/divides_sigma_p_to_eq.con
-cic:/matita/nat/neper/divides_pi_p_to_eq.con
-cic:/matita/nat/neper/divides_pi_p.con
-cic:/matita/nat/neper/divides_fact_fact.con
-cic:/matita/nat/nth_prime/smallest_factor_fact.con
-cic:/matita/nat/nth_prime/prime_to_nth_prime.con
-cic:/matita/nat/nth_prime/prime_nth_prime.con
-cic:/matita/nat/nth_prime/nth_prime.con
-cic:/matita/nat/nth_prime/lt_nth_prime_to_not_prime.con
-cic:/matita/nat/nth_prime/lt_nth_prime_n_nth_prime_Sn.con
-cic:/matita/nat/nth_prime/lt_n_nth_prime_n.con
-cic:/matita/nat/nth_prime/lt_SO_nth_prime_n.con
-cic:/matita/nat/nth_prime/lt_O_nth_prime_n.con
-cic:/matita/nat/nth_prime/injective_nth_prime.con
-cic:/matita/nat/nth_prime/increasing_nth_prime.con
-cic:/matita/nat/nth_prime/ex_prime.con
-cic:/matita/nat/nth_prime/ex_m_le_n_nth_prime_m.con
-cic:/matita/nat/o/lt_times_SSO_n_exp_SSO_n.con
-cic:/matita/nat/o/lt_exp_n_SSO_exp_SSO_n.con
-cic:/matita/nat/o/le_times_n_exp.con
-cic:/matita/nat/o/le_times_exp_n_SSO_exp_SSO_n.con
-cic:/matita/nat/o/le_times_SSO_n_exp_SSO_n.con
-cic:/matita/nat/o/le_exp_n_SSO_exp_SSO_n1.con
-cic:/matita/nat/o/le_exp_n_SSO_exp_SSO_n.con
-cic:/matita/nat/ord/p_ord_to_not_eq_O.con
-cic:/matita/nat/ord/p_ord_to_exp1.con
-cic:/matita/nat/ord/p_ord_times.con
-cic:/matita/nat/ord/p_ord_p.con
-cic:/matita/nat/ord/p_ord_inv.con
-cic:/matita/nat/ord/p_ord_exp1.con
-cic:/matita/nat/ord/p_ord_exp.con
-cic:/matita/nat/ord/p_ord_aux_to_not_mod_O.con
-cic:/matita/nat/ord/p_ord_aux_to_exp.con
-cic:/matita/nat/ord/p_ord_aux_to_Prop1.con
-cic:/matita/nat/ord/p_ord_aux_to_Prop.con
-cic:/matita/nat/ord/p_ord_aux.con
-cic:/matita/nat/ord/p_ord_O_to_not_divides.con
-cic:/matita/nat/ord/p_ord.con
-cic:/matita/nat/ord/ord_times.con
-cic:/matita/nat/ord/ord_rem.con
-cic:/matita/nat/ord/ord_ord_rem.con
-cic:/matita/nat/ord/ord_exp.con
-cic:/matita/nat/ord/ord_O_to_not_divides.con
-cic:/matita/nat/ord/ord.con
-cic:/matita/nat/ord/not_ord_O_to_divides.con
-cic:/matita/nat/ord/not_divides_to_p_ord_O.con
-cic:/matita/nat/ord/not_divides_to_ord_O.con
-cic:/matita/nat/ord/not_divides_ord_rem.con
-cic:/matita/nat/ord/mod_p_ord_inv.con
-cic:/matita/nat/ord/lt_ord_rem.con
-cic:/matita/nat/ord/lt_O_ord_rem.con
-cic:/matita/nat/ord/fst_p_ord_times.con
-cic:/matita/nat/ord/exp_ord.con
-cic:/matita/nat/ord/eq_p_ord_inv.con
-cic:/matita/nat/ord/divides_to_p_ord.con
-cic:/matita/nat/ord/divides_to_ord.con
-cic:/matita/nat/ord/divides_to_not_ord_O.con
-cic:/matita/nat/ord/divides_to_le_ord.con
-cic:/matita/nat/ord/divides_to_divides_ord_rem.con
-cic:/matita/nat/ord/divides_ord_rem.con
-cic:/matita/nat/ord/div_p_ord_inv.con
-cic:/matita/nat/orders/transitive_lt.con
-cic:/matita/nat/orders/transitive_le.con
-cic:/matita/nat/orders/trans_lt.con
-cic:/matita/nat/orders/trans_le.con
-cic:/matita/nat/orders/not_lt_to_le.con
-cic:/matita/nat/orders/not_le_to_lt.con
-cic:/matita/nat/orders/not_le_Sn_n.con
-cic:/matita/nat/orders/not_le_Sn_O.con
-cic:/matita/nat/orders/not_eq_to_le_to_lt.con
-cic:/matita/nat/orders/nat_elim1.con
-cic:/matita/nat/orders/ltn_to_ltO.con
-cic:/matita/nat/orders/lt_to_not_le.con
-cic:/matita/nat/orders/lt_to_not_eq.con
-cic:/matita/nat/orders/lt_to_lt_S_S.con
-cic:/matita/nat/orders/lt_to_le_to_lt.con
-cic:/matita/nat/orders/lt_to_le.con
-cic:/matita/nat/orders/lt_pred.con
-cic:/matita/nat/orders/lt_n_m_to_not_lt_m_Sn.con
-cic:/matita/nat/orders/lt_S_to_lt.con
-cic:/matita/nat/orders/lt_S_to_le.con
-cic:/matita/nat/orders/lt_S_S_to_lt.con
-cic:/matita/nat/orders/lt_SO_n_to_lt_O_pred_n.con
-cic:/matita/nat/orders/lt_O_n_elim.con
-cic:/matita/nat/orders/lt_O_S.con
-cic:/matita/nat/orders/lt.con
-cic:/matita/nat/orders/le_to_or_lt_eq.con
-cic:/matita/nat/orders/le_to_not_lt.con
-cic:/matita/nat/orders/le_to_lt_to_lt.con
-cic:/matita/nat/orders/le_to_le_to_eq.con
-cic:/matita/nat/orders/le_to_le_pred.con
-cic:/matita/nat/orders/le_pred_to_le.con
-cic:/matita/nat/orders/le_pred_n.con
-cic:/matita/nat/orders/le_n_m_to_lt_m_Sn_to_eq_n_m.con
-cic:/matita/nat/orders/le_n_fn.con
-cic:/matita/nat/orders/le_n_Sn.con
-cic:/matita/nat/orders/le_n_Sm_elim.con
-cic:/matita/nat/orders/le_n_O_to_eq.con
-cic:/matita/nat/orders/le_n_O_elim.con
-cic:/matita/nat/orders/le_inv.con
-cic:/matita/nat/orders/le_ind.con
-cic:/matita/nat/orders/le_S_S_to_le.con
-cic:/matita/nat/orders/le_S_S.con
-cic:/matita/nat/orders/le_O_n.con
-cic:/matita/nat/orders/leS_to_not_zero.con
-cic:/matita/nat/orders/le.ind
-cic:/matita/nat/orders/increasing_to_monotonic.con
-cic:/matita/nat/orders/increasing_to_le2.con
-cic:/matita/nat/orders/increasing_to_le.con
-cic:/matita/nat/orders/increasing.con
-cic:/matita/nat/orders/gt.con
-cic:/matita/nat/orders/ge.con
-cic:/matita/nat/orders/eq_to_not_lt.con
-cic:/matita/nat/orders/decidable_lt.con
-cic:/matita/nat/orders/decidable_le.con
-cic:/matita/nat/orders/antisymmetric_le.con
-cic:/matita/nat/orders/antisym_le.con
-cic:/matita/nat/orders/S_pred.con
-cic:/matita/nat/orders/Not_lt_n_n.con
-cic:/matita/nat/permutation/transpose_transpose.con
-cic:/matita/nat/permutation/transpose_i_j_j_i.con
-cic:/matita/nat/permutation/transpose_i_j_j.con
-cic:/matita/nat/permutation/transpose_i_j_i.con
-cic:/matita/nat/permutation/transpose_i_i.con
-cic:/matita/nat/permutation/transpose.con
-cic:/matita/nat/permutation/permut_transpose_r.con
-cic:/matita/nat/permutation/permut_transpose_l.con
-cic:/matita/nat/permutation/permut_transpose.con
-cic:/matita/nat/permutation/permut_to_eq_map_iter_i.con
-cic:/matita/nat/permutation/permut_to_bijn.con
-cic:/matita/nat/permutation/permut_n_to_le.con
-cic:/matita/nat/permutation/permut_n_to_eq_n.con
-cic:/matita/nat/permutation/permut_invert_permut.con
-cic:/matita/nat/permutation/permut_fg.con
-cic:/matita/nat/permutation/permut_S_to_permut_transpose.con
-cic:/matita/nat/permutation/permut_S_to_permut.con
-cic:/matita/nat/permutation/permut_O_to_eq_O.con
-cic:/matita/nat/permutation/permut.con
-cic:/matita/nat/permutation/map_iter_i.con
-cic:/matita/nat/permutation/invert_permut_f.con
-cic:/matita/nat/permutation/invert_permut.con
-cic:/matita/nat/permutation/injn_Sn_n.con
-cic:/matita/nat/permutation/injn.con
-cic:/matita/nat/permutation/injective_transpose.con
-cic:/matita/nat/permutation/injective_to_injn.con
-cic:/matita/nat/permutation/injective_invert_permut.con
-cic:/matita/nat/permutation/inj_transpose.con
-cic:/matita/nat/permutation/f_invert_permut.con
-cic:/matita/nat/permutation/eq_transpose.con
-cic:/matita/nat/permutation/eq_to_bijn.con
-cic:/matita/nat/permutation/eq_map_iter_i_transpose_l.con
-cic:/matita/nat/permutation/eq_map_iter_i_transpose_i_Si.con
-cic:/matita/nat/permutation/eq_map_iter_i_transpose2.con
-cic:/matita/nat/permutation/eq_map_iter_i_transpose1.con
-cic:/matita/nat/permutation/eq_map_iter_i_transpose.con
-cic:/matita/nat/permutation/eq_map_iter_i_sigma.con
-cic:/matita/nat/permutation/eq_map_iter_i_pi.con
-cic:/matita/nat/permutation/eq_map_iter_i_fact.con
-cic:/matita/nat/permutation/eq_map_iter_i.con
-cic:/matita/nat/permutation/bijn_transpose_r.con
-cic:/matita/nat/permutation/bijn_transpose_l.con
-cic:/matita/nat/permutation/bijn_transpose.con
-cic:/matita/nat/permutation/bijn_n_Sn.con
-cic:/matita/nat/permutation/bijn_fg.con
-cic:/matita/nat/permutation/bijn_Sn_n.con
-cic:/matita/nat/permutation/bijn.con
-cic:/matita/nat/pi_p/true_to_pi_p_Sn.con
-cic:/matita/nat/pi_p/times_pi_p.con
-cic:/matita/nat/pi_p/pi_p_times.con
-cic:/matita/nat/pi_p/pi_p_pi_p1.con
-cic:/matita/nat/pi_p/pi_p_pi_p.con
-cic:/matita/nat/pi_p/pi_p_knm.con
-cic:/matita/nat/pi_p/pi_p_gi.con
-cic:/matita/nat/pi_p/pi_p_false.con
-cic:/matita/nat/pi_p/pi_p_SO.con
-cic:/matita/nat/pi_p/pi_p2.con
-cic:/matita/nat/pi_p/pi_p2'.con
-cic:/matita/nat/pi_p/pi_p.con
-cic:/matita/nat/pi_p/or_false_eq_SO_to_eq_pi_p.con
-cic:/matita/nat/pi_p/le_pi_p.con
-cic:/matita/nat/pi_p/false_to_pi_p_Sn.con
-cic:/matita/nat/pi_p/false_to_eq_pi_p.con
-cic:/matita/nat/pi_p/exp_times_pi_p.con
-cic:/matita/nat/pi_p/exp_sigma_p1.con
-cic:/matita/nat/pi_p/exp_sigma_p.con
-cic:/matita/nat/pi_p/exp_pi_p.con
-cic:/matita/nat/pi_p/eq_pi_p_gh.con
-cic:/matita/nat/pi_p/eq_pi_p1.con
-cic:/matita/nat/pi_p/eq_pi_p.con
-cic:/matita/nat/plus/sym_plus.con
-cic:/matita/nat/plus/plus_n_Sm.con
-cic:/matita/nat/plus/plus_n_SO.con
-cic:/matita/nat/plus/plus_n_O.con
-cic:/matita/nat/plus/plus.con
-cic:/matita/nat/plus/injective_plus_r.con
-cic:/matita/nat/plus/injective_plus_l.con
-cic:/matita/nat/plus/inj_plus_r.con
-cic:/matita/nat/plus/inj_plus_l.con
-cic:/matita/nat/plus/associative_plus.con
-cic:/matita/nat/plus/assoc_plus.con
-cic:/matita/nat/primes/transitive_divides.con
-cic:/matita/nat/primes/trans_divides.con
-cic:/matita/nat/primes/smallest_factor.con
-cic:/matita/nat/primes/reflexive_divides.con
-cic:/matita/nat/primes/primeb_true_to_prime.con
-cic:/matita/nat/primes/primeb_to_Prop.con
-cic:/matita/nat/primes/primeb_false_to_not_prime.con
-cic:/matita/nat/primes/primeb.con
-cic:/matita/nat/primes/prime_to_smallest_factor.con
-cic:/matita/nat/primes/prime_to_primeb_true.con
-cic:/matita/nat/primes/prime_to_lt_SO.con
-cic:/matita/nat/primes/prime_to_lt_O.con
-cic:/matita/nat/primes/prime_smallest_factor_n.con
-cic:/matita/nat/primes/prime.con
-cic:/matita/nat/primes/or_div_mod1.con
-cic:/matita/nat/primes/not_prime_to_primeb_false.con
-cic:/matita/nat/primes/not_prime_SO.con
-cic:/matita/nat/primes/not_prime_O.con
-cic:/matita/nat/primes/not_divides_to_divides_b_false.con
-cic:/matita/nat/primes/not_divides_S_fact.con
-cic:/matita/nat/primes/mod_S_fact.con
-cic:/matita/nat/primes/mod_O_to_divides.con
-cic:/matita/nat/primes/lt_smallest_factor_to_not_divides.con
-cic:/matita/nat/primes/lt_SO_smallest_factor.con
-cic:/matita/nat/primes/lt_O_smallest_factor.con
-cic:/matita/nat/primes/le_smallest_factor_n.con
-cic:/matita/nat/primes/eq_mod_to_divides.con
-cic:/matita/nat/primes/eq_div_plus.con
-cic:/matita/nat/primes/divides_to_mod_O.con
-cic:/matita/nat/primes/divides_to_lt_O.con
-cic:/matita/nat/primes/divides_to_le.con
-cic:/matita/nat/primes/divides_to_eq_times_div_div_times.con
-cic:/matita/nat/primes/divides_to_divides_b_true1.con
-cic:/matita/nat/primes/divides_to_divides_b_true.con
-cic:/matita/nat/primes/divides_to_div_mod_spec.con
-cic:/matita/nat/primes/divides_to_div.con
-cic:/matita/nat/primes/divides_times.con
-cic:/matita/nat/primes/divides_smallest_factor_n.con
-cic:/matita/nat/primes/divides_plus.con
-cic:/matita/nat/primes/divides_n_n.con
-cic:/matita/nat/primes/divides_n_O.con
-cic:/matita/nat/primes/divides_minus.con
-cic:/matita/nat/primes/divides_ind.con
-cic:/matita/nat/primes/divides_fact.con
-cic:/matita/nat/primes/divides_f_pi_f.con
-cic:/matita/nat/primes/divides_div.con
-cic:/matita/nat/primes/divides_b_true_to_lt_O.con
-cic:/matita/nat/primes/divides_b_true_to_divides1.con
-cic:/matita/nat/primes/divides_b_true_to_divides.con
-cic:/matita/nat/primes/divides_b_to_Prop.con
-cic:/matita/nat/primes/divides_b_false_to_not_divides1.con
-cic:/matita/nat/primes/divides_b_false_to_not_divides.con
-cic:/matita/nat/primes/divides_b_div_true.con
-cic:/matita/nat/primes/divides_b.con
-cic:/matita/nat/primes/divides_SO_n.con
-cic:/matita/nat/primes/divides.ind
-cic:/matita/nat/primes/div_mod_spec_to_divides.con
-cic:/matita/nat/primes/div_div.con
-cic:/matita/nat/primes/decidable_prime.con
-cic:/matita/nat/primes/decidable_divides.con
-cic:/matita/nat/primes/antisymmetric_divides.con
-cic:/matita/nat/relevant_equations/times_plus_plus.con
-cic:/matita/nat/relevant_equations/times_plus_l.con
-cic:/matita/nat/relevant_equations/times_minus_l.con
-cic:/matita/nat/relevant_equations/eq_pred_to_eq.con
-cic:/matita/nat/sigma_and_pi/sigma.con
-cic:/matita/nat/sigma_and_pi/pi.con
-cic:/matita/nat/sigma_and_pi/exp_pi_l.con
-cic:/matita/nat/sigma_and_pi/eq_sigma.con
-cic:/matita/nat/sigma_and_pi/eq_pi.con
-cic:/matita/nat/sigma_and_pi/eq_fact_pi.con
-cic:/matita/nat/sqrt/sqrt.con
-cic:/matita/nat/sqrt/monotonic_sqrt.con
-cic:/matita/nat/sqrt/lt_sqrt_to_le_times_l.con
-cic:/matita/nat/sqrt/lt_sqrt_n.con
-cic:/matita/nat/sqrt/lt_sqrt.con
-cic:/matita/nat/sqrt/leq_sqrt_n.con
-cic:/matita/nat/sqrt/le_sqrt_to_le_times_r.con
-cic:/matita/nat/sqrt/le_sqrt_to_le_times_l.con
-cic:/matita/nat/sqrt/le_sqrt_nl.con
-cic:/matita/nat/sqrt/le_sqrt_n_n.con
-cic:/matita/nat/sqrt/le_sqrt_n1.con
-cic:/matita/nat/sqrt/le_sqrt_log_n.con
-cic:/matita/nat/sqrt/eq_sqrt.con
-cic:/matita/nat/times/times_n_Sm.con
-cic:/matita/nat/times/times_n_SO.con
-cic:/matita/nat/times/times_n_O.con
-cic:/matita/nat/times/times_SSO_n.con
-cic:/matita/nat/times/times_SSO.con
-cic:/matita/nat/times/times_O_to_O.con
-cic:/matita/nat/times/times.con
-cic:/matita/nat/times/symmetric_times.con
-cic:/matita/nat/times/sym_times.con
-cic:/matita/nat/times/or_eq_eq_S.con
-cic:/matita/nat/times/distributive_times_plus.con
-cic:/matita/nat/times/distr_times_plus.con
-cic:/matita/nat/times/associative_times.con
-cic:/matita/nat/times/assoc_times.con
-cic:/matita/nat/totient/totient_times.con
-cic:/matita/nat/totient/totient.con
-cic:/matita/nat/totient1/sigma_p_Sn_divides_b_totient_n.con
-cic:/matita/nat/totient1/lt_O_to_divides_to_lt_O_div.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/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/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/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/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.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/technicalities/setoids/variance_rect.con
-cic:/matita/technicalities/setoids/variance_rec.con
-cic:/matita/technicalities/setoids/variance_of_argument_class.con
-cic:/matita/technicalities/setoids/variance_ind.con
-cic:/matita/technicalities/setoids/variance.ind
-cic:/matita/technicalities/setoids/rewrite_direction_rect.con
-cic:/matita/technicalities/setoids/rewrite_direction_rec.con
-cic:/matita/technicalities/setoids/rewrite_direction_ind.con
-cic:/matita/technicalities/setoids/rewrite_direction.ind
-cic:/matita/technicalities/setoids/relation_of_relation_class.con
-cic:/matita/technicalities/setoids/relation_of_areflexive_relation_class.con
-cic:/matita/technicalities/setoids/relation_class_of_reflexive_relation_class.con
-cic:/matita/technicalities/setoids/relation_class_of_argument_class.con
-cic:/matita/technicalities/setoids/relation_class_of_areflexive_relation_class.con
-# # mutual fix
-# cic:/matita/demo/propositional_sequent_calculus/not_nf_elim_not.con
-# # depending on the previous
-# cic:/matita/demo/propositional_sequent_calculus/eq_eval_elim_not_eval.con
-# cic:/matita/demo/propositional_sequent_calculus/elim_not.con
-# cic:/matita/demo/propositional_sequent_calculus/distributive_orb_andb.con
-# cic:/matita/demo/propositional_sequent_calculus/distributive_andb_orb.con
-# cic:/matita/demo/propositional_sequent_calculus/derive_inv.con
-# cic:/matita/demo/propositional_sequent_calculus/derive_ind.con
-# cic:/matita/demo/propositional_sequent_calculus/derive.ind
-# cic:/matita/demo/propositional_sequent_calculus/demorgan2.con
-# cic:/matita/demo/propositional_sequent_calculus/demorgan1.con
-# cic:/matita/demo/propositional_sequent_calculus/daemon.con
-# cic:/matita/demo/propositional_sequent_calculus/completeness_base.con
-# cic:/matita/demo/propositional_sequent_calculus/associative_andb.con
-# cic:/matita/demo/propositional_sequent_calculus/assoc_orb.con
-# cic:/matita/demo/propositional_sequent_calculus/and_of_list_permut.con
-# cic:/matita/demo/propositional_sequent_calculus/and_of_list.con
-# cic:/matita/demo/propositional_sequent_calculus/Formula_rect.con
-# cic:/matita/demo/propositional_sequent_calculus/Formula_rec.con
-# cic:/matita/demo/propositional_sequent_calculus/Formula_ind.con
-# cic:/matita/demo/propositional_sequent_calculus/Formula.ind
-# # universe inferece missing
-# cic:/matita/technicalities/setoids/relation_of_product_of_arguments.con
-# cic:/matita/technicalities/setoids/product_of_arguments.con
-# cic:/matita/technicalities/setoids/opposite_direction_idempotent.con
-# cic:/matita/technicalities/setoids/opposite_direction.con
-# cic:/matita/technicalities/setoids/nelistT_rect.con
-# cic:/matita/technicalities/setoids/nelistT_rec.con
-# cic:/matita/technicalities/setoids/nelistT_ind.con
-# cic:/matita/technicalities/setoids/nelistT.ind
-# cic:/matita/technicalities/setoids/morphism_theory_of_predicate.con
-# cic:/matita/technicalities/setoids/morphism_theory_of_function.con
-# cic:/matita/technicalities/setoids/make_compatibility_goal_aux.con
-# cic:/matita/technicalities/setoids/make_compatibility_goal.con
-# cic:/matita/technicalities/setoids/list_of_Leibniz_of_list_of_types.con
-# cic:/matita/technicalities/setoids/interp_relation_class_list.con
-# cic:/matita/technicalities/setoids/interp.con
-# cic:/matita/technicalities/setoids/impl_trans.con
-# cic:/matita/technicalities/setoids/impl_refl.con
-# cic:/matita/technicalities/setoids/impl.con
-# cic:/matita/technicalities/setoids/get_rewrite_direction.con
-# cic:/matita/technicalities/setoids/function_type_of_morphism_signature.con
-# cic:/matita/technicalities/setoids/equality_morphism_of_symmetric_reflexive_transitive_relation.con
-# cic:/matita/technicalities/setoids/equality_morphism_of_symmetric_areflexive_transitive_relation.con
-# cic:/matita/technicalities/setoids/equality_morphism_of_asymmetric_reflexive_transitive_relation.con
-# cic:/matita/technicalities/setoids/equality_morphism_of_asymmetric_areflexive_transitive_relation.con
-# cic:/matita/technicalities/setoids/directed_relation_of_relation_class.con
-# cic:/matita/technicalities/setoids/directed_relation_of_argument_class.con
-# cic:/matita/technicalities/setoids/check_if_variance_is_respected_inv.con
-# cic:/matita/technicalities/setoids/check_if_variance_is_respected_ind.con
-# cic:/matita/technicalities/setoids/check_if_variance_is_respected.ind
-# cic:/matita/technicalities/setoids/carrier_of_relation_class.con
-# cic:/matita/technicalities/setoids/carrier_of_reflexive_relation_class.con
-# cic:/matita/technicalities/setoids/carrier_of_areflexive_relation_class.con
-# cic:/matita/technicalities/setoids/apply_morphism_compatibility_Right2Left.con
-# cic:/matita/technicalities/setoids/apply_morphism_compatibility_Left2Right.con
-# cic:/matita/technicalities/setoids/apply_morphism.con
-# cic:/matita/technicalities/setoids/about_carrier_of_relation_class_and_relation_class_of_argument_class.con
-# cic:/matita/technicalities/setoids/X_Relation_Class_rect.con
-# cic:/matita/technicalities/setoids/X_Relation_Class_rec.con
-# cic:/matita/technicalities/setoids/X_Relation_Class_ind.con
-# cic:/matita/technicalities/setoids/X_Relation_Class.ind
-# cic:/matita/technicalities/setoids/Relation_Class.con
-# cic:/matita/technicalities/setoids/Reflexive_Relation_Class_rect.con
-# cic:/matita/technicalities/setoids/Reflexive_Relation_Class_rec.con
-# cic:/matita/technicalities/setoids/Reflexive_Relation_Class_ind.con
-# cic:/matita/technicalities/setoids/Reflexive_Relation_Class.ind
-# cic:/matita/technicalities/setoids/Morphism_Theory_rect.con
-# cic:/matita/technicalities/setoids/Morphism_Theory_rec.con
-# cic:/matita/technicalities/setoids/Morphism_Theory_ind.con
-# cic:/matita/technicalities/setoids/Morphism_Theory.ind
-# cic:/matita/technicalities/setoids/Morphism_Context_rect2.con
-# cic:/matita/technicalities/setoids/Morphism_Context_rect.con
-# cic:/matita/technicalities/setoids/Morphism_Context_rec.con
-# cic:/matita/technicalities/setoids/Morphism_Context_inv.con
-# cic:/matita/technicalities/setoids/Morphism_Context_ind.con
-# cic:/matita/technicalities/setoids/Morphism_Context_List_rect2.con
-# cic:/matita/technicalities/setoids/Morphism_Context_List_rect.con
-# cic:/matita/technicalities/setoids/Morphism_Context_List_rec.con
-# cic:/matita/technicalities/setoids/Morphism_Context_List_inv.con
-# cic:/matita/technicalities/setoids/Morphism_Context_List_ind.con
-# cic:/matita/technicalities/setoids/Morphism_Context.ind
-# cic:/matita/technicalities/setoids/Impl_Relation_Class.con
-# cic:/matita/technicalities/setoids/Iff_Relation_Class.con
-# cic:/matita/technicalities/setoids/Function.con
-# cic:/matita/technicalities/setoids/Compat.con
-# cic:/matita/technicalities/setoids/Arguments.con
-# cic:/matita/technicalities/setoids/Argument_Class.con
-# cic:/matita/technicalities/setoids/Areflexive_Relation_Class_rect.con
-# cic:/matita/technicalities/setoids/Areflexive_Relation_Class_rec.con
-# cic:/matita/technicalities/setoids/Areflexive_Relation_Class_ind.con
-# cic:/matita/technicalities/setoids/Areflexive_Relation_Class.ind