1 cic:/CoRN/algebra/Basics/well_founded_ltof.con
2 cic:/CoRN/algebra/Basics/well_founded_induction_type.con
3 cic:/CoRN/algebra/Basics/well_founded.con
4 cic:/CoRN/algebra/Basics/surj_not.con
5 cic:/CoRN/algebra/Basics/surj_lt_subproof.con
6 cic:/CoRN/algebra/Basics/surj_lt.con
7 cic:/CoRN/algebra/Basics/surj_le_subproof.con
8 cic:/CoRN/algebra/Basics/surj_le.con
9 cic:/CoRN/algebra/Basics/surj_eq_subproof.con
10 cic:/CoRN/algebra/Basics/surj_eq.con
11 cic:/CoRN/algebra/Basics/proper_caseZ_diff_subproof0.con
12 cic:/CoRN/algebra/Basics/proper_caseZ_diff_subproof.con
13 cic:/CoRN/algebra/Basics/proper_caseZ_diff.con
14 cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con
15 cic:/CoRN/algebra/Basics/power.con
16 cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con
17 cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con
18 cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con
19 cic:/CoRN/algebra/Basics/nats_Z_ind.con
20 cic:/CoRN/algebra/Basics/nat_fac_gtzero.con
21 cic:/CoRN/algebra/Basics/minus4_subproof1.con
22 cic:/CoRN/algebra/Basics/minus4_subproof0.con
23 cic:/CoRN/algebra/Basics/minus4_subproof.con
24 cic:/CoRN/algebra/Basics/minus4.con
25 cic:/CoRN/algebra/Basics/minus3_subproof1.con
26 cic:/CoRN/algebra/Basics/minus3_subproof0.con
27 cic:/CoRN/algebra/Basics/minus3_subproof.con
28 cic:/CoRN/algebra/Basics/minus3.con
29 cic:/CoRN/algebra/Basics/min_convert_is_NEG.con
30 cic:/CoRN/algebra/Basics/ltof.con
31 cic:/CoRN/algebra/Basics/lt_z_two.con
32 cic:/CoRN/algebra/Basics/lt_wf_rect.con
33 cic:/CoRN/algebra/Basics/lt_mult_right.con
34 cic:/CoRN/algebra/Basics/lt_lt_minus_subproof.con
35 cic:/CoRN/algebra/Basics/lt_lt_minus.con
36 cic:/CoRN/algebra/Basics/lt_le_dec.con
37 cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con
38 cic:/CoRN/algebra/Basics/le_pred.con
39 cic:/CoRN/algebra/Basics/le_mult_right.con
40 cic:/CoRN/algebra/Basics/inject_nat_convert.con
41 cic:/CoRN/algebra/Basics/induction_ltof2T.con
42 cic:/CoRN/algebra/Basics/fac.con
43 cic:/CoRN/algebra/Basics/diff_Z_ind_subproof.con
44 cic:/CoRN/algebra/Basics/diff_Z_ind.con
45 cic:/CoRN/algebra/Basics/convert_is_POS.con
46 cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con
47 cic:/CoRN/algebra/Basics/caseZ_diff_O.con
48 cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con
49 cic:/CoRN/algebra/Basics/caseZ_diff.con
50 cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con
51 cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con
52 cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con
53 cic:/CoRN/algebra/Basics/Zmult_absorb.con
54 cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con
55 cic:/CoRN/algebra/Basics/Zlt_opp.con
56 cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con
57 cic:/CoRN/algebra/Basics/Zgt_not_eq.con
58 cic:/CoRN/algebra/Basics/Z_to_nat_correct.con
59 cic:/CoRN/algebra/Basics/Z_to_nat.con
60 cic:/CoRN/algebra/Basics/Z_exh.con
61 cic:/CoRN/algebra/Basics/POS_anti_convert.con
62 cic:/CoRN/algebra/Basics/NEG_anti_convert.con
63 cic:/CoRN/algebra/Basics/Acc_iter.con
64 cic:/CoRN/algebra/Basics/Acc_inv.con
65 cic:/CoRN/algebra/Basics/Acc_ind.con
66 cic:/CoRN/algebra/Basics/Acc.ind
67 cic:/CoRN/algebra/CAbGroups/zmult_zero.con
68 cic:/CoRN/algebra/CAbGroups/zmult_wd.con
69 cic:/CoRN/algebra/CAbGroups/zmult_plus.con
70 cic:/CoRN/algebra/CAbGroups/zmult_plus'.con
71 cic:/CoRN/algebra/CAbGroups/zmult_one.con
72 cic:/CoRN/algebra/CAbGroups/zmult_mult.con
73 cic:/CoRN/algebra/CAbGroups/zmult_min_one.con
74 cic:/CoRN/algebra/CAbGroups/zmult_char_subproof1.con
75 cic:/CoRN/algebra/CAbGroups/zmult_char_subproof0.con
76 cic:/CoRN/algebra/CAbGroups/zmult_char_subproof.con
77 cic:/CoRN/algebra/CAbGroups/zmult_char.con
78 cic:/CoRN/algebra/CAbGroups/zmult_Zero.con
79 cic:/CoRN/algebra/CAbGroups/zmult.con
80 cic:/CoRN/algebra/CAbGroups/plus_runit.con
81 cic:/CoRN/algebra/CAbGroups/plus_rext.con
82 cic:/CoRN/algebra/CAbGroups/plus_is_fun.con
83 cic:/CoRN/algebra/CAbGroups/plus_fun.con
84 cic:/CoRN/algebra/CAbGroups/plus_cancel_ap_lft.con
85 cic:/CoRN/algebra/CAbGroups/op_lft_resp_ap.con
86 cic:/CoRN/algebra/CAbGroups/nmult_wd.con
87 cic:/CoRN/algebra/CAbGroups/nmult_plus.con
88 cic:/CoRN/algebra/CAbGroups/nmult_plus'.con
89 cic:/CoRN/algebra/CAbGroups/nmult_one.con
90 cic:/CoRN/algebra/CAbGroups/nmult_mult.con
91 cic:/CoRN/algebra/CAbGroups/nmult_inv.con
92 cic:/CoRN/algebra/CAbGroups/nmult_Zero.con
93 cic:/CoRN/algebra/CAbGroups/nmult.con
94 cic:/CoRN/algebra/CAbGroups/minus_plus.con
95 cic:/CoRN/algebra/CAbGroups/isabgrp_scrr.con
96 cic:/CoRN/algebra/CAbGroups/is_CAbGroup.con
97 cic:/CoRN/algebra/CAbGroups/inv_inv'.con
98 cic:/CoRN/algebra/CAbGroups/cag_proof.con
99 cic:/CoRN/algebra/CAbGroups/cag_op_inv.con
100 cic:/CoRN/algebra/CAbGroups/cag_crr.con
101 cic:/CoRN/algebra/CAbGroups/cag_commutes_unfolded.con
102 cic:/CoRN/algebra/CAbGroups/cag_commutes.con
103 cic:/CoRN/algebra/CAbGroups/cag_ap_cancel_lft.con
104 cic:/CoRN/algebra/CAbGroups/assoc_1.con
105 cic:/CoRN/algebra/CAbGroups/CAbGroup_rect.con
106 cic:/CoRN/algebra/CAbGroups/CAbGroup_rec.con
107 cic:/CoRN/algebra/CAbGroups/CAbGroup_is_CAbGroup.con
108 cic:/CoRN/algebra/CAbGroups/CAbGroup_ind.con
109 cic:/CoRN/algebra/CAbGroups/CAbGroup.ind
110 cic:/CoRN/algebra/CAbGroups/Build_SubCAbGroup.con
111 cic:/CoRN/algebra/CAbGroups/Build_CSemiGroup'.con
112 cic:/CoRN/algebra/CAbGroups/Build_CMonoid'.con
113 cic:/CoRN/algebra/CAbGroups/Build_CGroup'.con
114 cic:/CoRN/algebra/CAbGroups/Build_CAbGroup'.con
115 cic:/CoRN/algebra/CAbMonoids/isabgrp_scrr.con
116 cic:/CoRN/algebra/CAbMonoids/is_CAbMonoid.con
117 cic:/CoRN/algebra/CAbMonoids/cam_proof.con
118 cic:/CoRN/algebra/CAbMonoids/cam_crr.con
119 cic:/CoRN/algebra/CAbMonoids/cam_commutes_unfolded.con
120 cic:/CoRN/algebra/CAbMonoids/cam_commutes.con
121 cic:/CoRN/algebra/CAbMonoids/CAbMonoid_rect.con
122 cic:/CoRN/algebra/CAbMonoids/CAbMonoid_rec.con
123 cic:/CoRN/algebra/CAbMonoids/CAbMonoid_is_CAbMonoid.con
124 cic:/CoRN/algebra/CAbMonoids/CAbMonoid_ind.con
125 cic:/CoRN/algebra/CAbMonoids/CAbMonoid.ind
126 cic:/CoRN/algebra/CAbMonoids/Build_SubCAbMonoid.con
127 cic:/CoRN/algebra/CHomomorphism_Theorems/tau_surj.con
128 cic:/CoRN/algebra/CHomomorphism_Theorems/tau_strext.con
129 cic:/CoRN/algebra/CHomomorphism_Theorems/tau_is_fun.con
130 cic:/CoRN/algebra/CHomomorphism_Theorems/tau.con
131 cic:/CoRN/algebra/CHomomorphism_Theorems/sigst_strext.con
132 cic:/CoRN/algebra/CHomomorphism_Theorems/sigst_is_fun.con
133 cic:/CoRN/algebra/CHomomorphism_Theorems/sigst_inj.con
134 cic:/CoRN/algebra/CHomomorphism_Theorems/sigst.con
135 cic:/CoRN/algebra/CHomomorphism_Theorems/cswdpredR.con
136 cic:/CoRN/algebra/CHomomorphism_Theorems/cswdpred.con
137 cic:/CoRN/algebra/CHomomorphism_Theorems/cspredR.con
138 cic:/CoRN/algebra/CHomomorphism_Theorems/cspred.con
139 cic:/CoRN/algebra/CHomomorphism_Theorems/cs_is_comod.con
140 cic:/CoRN/algebra/CHomomorphism_Theorems/cs_is_coideal.con
141 cic:/CoRN/algebra/CHomomorphism_Theorems/cs_as_comod.con
142 cic:/CoRN/algebra/CHomomorphism_Theorems/cs_as_coideal.con
143 cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau_surj.con
144 cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau_strext.con
145 cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau_is_fun.con
146 cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau.con
147 cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst_strext.con
148 cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst_is_fun.con
149 cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst_inj.con
150 cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst.con
151 cic:/CoRN/algebra/CHomomorphism_Theorems/RingHomTheorem.con
152 cic:/CoRN/algebra/CHomomorphism_Theorems/RdivCsR.con
153 cic:/CoRN/algebra/CHomomorphism_Theorems/ModHomTheorem.con
154 cic:/CoRN/algebra/CHomomorphism_Theorems/CsR.con
155 cic:/CoRN/algebra/CHomomorphism_Theorems/Cs.con
156 cic:/CoRN/algebra/CHomomorphism_Theorems/AdivCs.con
157 cic:/CoRN/algebra/CIdeals/is_ideal_rect.con
158 cic:/CoRN/algebra/CIdeals/is_ideal_rec.con
159 cic:/CoRN/algebra/CIdeals/is_ideal_ind.con
160 cic:/CoRN/algebra/CIdeals/is_ideal.ind
161 cic:/CoRN/algebra/CIdeals/is_coideal_rect.con
162 cic:/CoRN/algebra/CIdeals/is_coideal_rec.con
163 cic:/CoRN/algebra/CIdeals/is_coideal_ind.con
164 cic:/CoRN/algebra/CIdeals/is_coideal.ind
165 cic:/CoRN/algebra/CIdeals/idprpl.con
166 cic:/CoRN/algebra/CIdeals/idproof.con
167 cic:/CoRN/algebra/CIdeals/idpred.con
168 cic:/CoRN/algebra/CIdeals/ideal_rect.con
169 cic:/CoRN/algebra/CIdeals/ideal_rec.con
170 cic:/CoRN/algebra/CIdeals/ideal_is_ideal.con
171 cic:/CoRN/algebra/CIdeals/ideal_ind.con
172 cic:/CoRN/algebra/CIdeals/ideal_as_CSetoid.con
173 cic:/CoRN/algebra/CIdeals/ideal.ind
174 cic:/CoRN/algebra/CIdeals/idax.con
175 cic:/CoRN/algebra/CIdeals/coideal_wd.con
176 cic:/CoRN/algebra/CIdeals/coideal_rect.con
177 cic:/CoRN/algebra/CIdeals/coideal_rec.con
178 cic:/CoRN/algebra/CIdeals/coideal_plus.con
179 cic:/CoRN/algebra/CIdeals/coideal_nonzero.con
180 cic:/CoRN/algebra/CIdeals/coideal_nontriv.con
181 cic:/CoRN/algebra/CIdeals/coideal_mult.con
182 cic:/CoRN/algebra/CIdeals/coideal_is_coideal.con
183 cic:/CoRN/algebra/CIdeals/coideal_ind.con
184 cic:/CoRN/algebra/CIdeals/coideal_as_CSetoid.con
185 cic:/CoRN/algebra/CIdeals/coideal_apzero.con
186 cic:/CoRN/algebra/CIdeals/coideal.ind
187 cic:/CoRN/algebra/CIdeals/ciproof.con
188 cic:/CoRN/algebra/CIdeals/cipred.con
189 cic:/CoRN/algebra/CIdeals/ciplus.con
190 cic:/CoRN/algebra/CIdeals/cinontriv.con
191 cic:/CoRN/algebra/CIdeals/cimult.con
192 cic:/CoRN/algebra/CIdeals/ciapzero.con
193 cic:/CoRN/algebra/CLogic/weird_mon_covers.con
194 cic:/CoRN/algebra/CLogic/to_Codd_even.con
195 cic:/CoRN/algebra/CLogic/to_Codd.con
196 cic:/CoRN/algebra/CLogic/to_Ceven.con
197 cic:/CoRN/algebra/CLogic/toCle.con
198 cic:/CoRN/algebra/CLogic/toCProp_rect.con
199 cic:/CoRN/algebra/CLogic/toCProp_rec.con
200 cic:/CoRN/algebra/CLogic/toCProp_lt.con
201 cic:/CoRN/algebra/CLogic/toCProp_ind.con
202 cic:/CoRN/algebra/CLogic/toCProp_e.con
203 cic:/CoRN/algebra/CLogic/toCProp_Zlt.con
204 cic:/CoRN/algebra/CLogic/toCProp.ind
205 cic:/CoRN/algebra/CLogic/str_finite_or_elim.con
206 cic:/CoRN/algebra/CLogic/sig2T_rect.con
207 cic:/CoRN/algebra/CLogic/sig2T_rec.con
208 cic:/CoRN/algebra/CLogic/sig2T_ind.con
209 cic:/CoRN/algebra/CLogic/sig2T.ind
210 cic:/CoRN/algebra/CLogic/proj2b_sig2T.con
211 cic:/CoRN/algebra/CLogic/proj2a_sig2T.con
212 cic:/CoRN/algebra/CLogic/proj2_sigT.con
213 cic:/CoRN/algebra/CLogic/proj1_sigT.con
214 cic:/CoRN/algebra/CLogic/proj1_sig2T.con
215 cic:/CoRN/algebra/CLogic/pred_lt.con
216 cic:/CoRN/algebra/CLogic/plus_pred_pred_plus.con
217 cic:/CoRN/algebra/CLogic/plus_eq_one_imp_eq_zero.con
218 cic:/CoRN/algebra/CLogic/odd_induction.con
219 cic:/CoRN/algebra/CLogic/odd_ind.con
220 cic:/CoRN/algebra/CLogic/odd_double_ind.con
221 cic:/CoRN/algebra/CLogic/not_r_sum_rec.con
222 cic:/CoRN/algebra/CLogic/not_r_cor_rect.con
223 cic:/CoRN/algebra/CLogic/not_not_lt.con
224 cic:/CoRN/algebra/CLogic/not_l_sum_rec.con
225 cic:/CoRN/algebra/CLogic/not_l_cor_rect.con
226 cic:/CoRN/algebra/CLogic/nat_nat_pos.con
227 cic:/CoRN/algebra/CLogic/nat_mon_imp_mon'.con
228 cic:/CoRN/algebra/CLogic/nat_mon_imp_inj.con
229 cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon_le.con
230 cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon.con
231 cic:/CoRN/algebra/CLogic/nat_less_n_pred.con
232 cic:/CoRN/algebra/CLogic/nat_less_n_pred'.con
233 cic:/CoRN/algebra/CLogic/nat_complete_double_induction.con
234 cic:/CoRN/algebra/CLogic/nat_complete_double_ind.con
235 cic:/CoRN/algebra/CLogic/my_Cle_ind.con
236 cic:/CoRN/algebra/CLogic/mon_fun_covers.con
237 cic:/CoRN/algebra/CLogic/member_app.con
238 cic:/CoRN/algebra/CLogic/member.con
239 cic:/CoRN/algebra/CLogic/lt_pred'.con
240 cic:/CoRN/algebra/CLogic/lt_8.con
241 cic:/CoRN/algebra/CLogic/lt_5.con
242 cic:/CoRN/algebra/CLogic/lt_10.con
243 cic:/CoRN/algebra/CLogic/le_2.con
244 cic:/CoRN/algebra/CLogic/le_1.con
245 cic:/CoRN/algebra/CLogic/kseq_prop.con
246 cic:/CoRN/algebra/CLogic/four_induction.con
247 cic:/CoRN/algebra/CLogic/four_ind.con
248 cic:/CoRN/algebra/CLogic/finite_or_elim.con
249 cic:/CoRN/algebra/CLogic/even_plus_n_n.con
250 cic:/CoRN/algebra/CLogic/even_or_odd_plus_gt.con
251 cic:/CoRN/algebra/CLogic/even_or_odd_plus.con
252 cic:/CoRN/algebra/CLogic/even_induction.con
253 cic:/CoRN/algebra/CLogic/even_ind.con
254 cic:/CoRN/algebra/CLogic/choice.con
255 cic:/CoRN/algebra/CLogic/absolu_2.con
256 cic:/CoRN/algebra/CLogic/absolu_1.con
257 cic:/CoRN/algebra/CLogic/Zsgn_5.con
258 cic:/CoRN/algebra/CLogic/Zsgn_4.con
259 cic:/CoRN/algebra/CLogic/Zsgn_3.con
260 cic:/CoRN/algebra/CLogic/Zsgn_2.con
261 cic:/CoRN/algebra/CLogic/Zsgn_1.con
262 cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con
263 cic:/CoRN/algebra/CLogic/Zlts.con
264 cic:/CoRN/algebra/CLogic/Zgt_mult_reg_absorb_l.con
265 cic:/CoRN/algebra/CLogic/Zgt_mult_conv_absorb_l.con
266 cic:/CoRN/algebra/CLogic/ZL9.con
267 cic:/CoRN/algebra/CLogic/ZL4'.con
268 cic:/CoRN/algebra/CLogic/Ttransitive.con
269 cic:/CoRN/algebra/CLogic/Tsymmetric.con
270 cic:/CoRN/algebra/CLogic/Trelation.con
271 cic:/CoRN/algebra/CLogic/Treflexive.con
272 cic:/CoRN/algebra/CLogic/Tequiv.con
273 cic:/CoRN/algebra/CLogic/S_predn.con
274 cic:/CoRN/algebra/CLogic/Not.con
275 cic:/CoRN/algebra/CLogic/Iff_trans.con
276 cic:/CoRN/algebra/CLogic/Iff_sym.con
277 cic:/CoRN/algebra/CLogic/Iff_right.con
278 cic:/CoRN/algebra/CLogic/Iff_refl.con
279 cic:/CoRN/algebra/CLogic/Iff_left.con
280 cic:/CoRN/algebra/CLogic/Iff_imp_imp.con
281 cic:/CoRN/algebra/CLogic/Iff.con
282 cic:/CoRN/algebra/CLogic/Ctransitive.con
283 cic:/CoRN/algebra/CLogic/Csymmetric.con
284 cic:/CoRN/algebra/CLogic/Crelation.con
285 cic:/CoRN/algebra/CLogic/Creflexive.con
286 cic:/CoRN/algebra/CLogic/Cpred_succ_Z_ind.con
287 cic:/CoRN/algebra/CLogic/Codd_to.con
288 cic:/CoRN/algebra/CLogic/Codd_rect.con
289 cic:/CoRN/algebra/CLogic/Codd_rec.con
290 cic:/CoRN/algebra/CLogic/Codd_ind.con
291 cic:/CoRN/algebra/CLogic/Codd_even_to.con
292 cic:/CoRN/algebra/CLogic/Codd.ind
293 cic:/CoRN/algebra/CLogic/Cnats_Z_ind.con
294 cic:/CoRN/algebra/CLogic/Cnat_total_order.con
295 cic:/CoRN/algebra/CLogic/Cnat_double_ind.con
296 cic:/CoRN/algebra/CLogic/Clt_to.con
297 cic:/CoRN/algebra/CLogic/Clt_le_weak.con
298 cic:/CoRN/algebra/CLogic/Clt.con
299 cic:/CoRN/algebra/CLogic/Cle_to.con
300 cic:/CoRN/algebra/CLogic/Cle_rect.con
301 cic:/CoRN/algebra/CLogic/Cle_rec.con
302 cic:/CoRN/algebra/CLogic/Cle_n_S.con
303 cic:/CoRN/algebra/CLogic/Cle_le_S_eq.con
304 cic:/CoRN/algebra/CLogic/Cle_ind.con
305 cic:/CoRN/algebra/CLogic/Cle.ind
306 cic:/CoRN/algebra/CLogic/Ceven_to.con
307 cic:/CoRN/algebra/CLogic/Ceven_rect.con
308 cic:/CoRN/algebra/CLogic/Ceven_rec.con
309 cic:/CoRN/algebra/CLogic/Ceven_ind.con
310 cic:/CoRN/algebra/CLogic/Cequiv.con
311 cic:/CoRN/algebra/CLogic/Cdiff_Z_ind_subproof.con
312 cic:/CoRN/algebra/CLogic/Cdiff_Z_ind.con
313 cic:/CoRN/algebra/CLogic/Cdecidable.con
314 cic:/CoRN/algebra/CLogic/CdeMorgan_ex_all.con
315 cic:/CoRN/algebra/CLogic/Ccontrapos'.con
316 cic:/CoRN/algebra/CLogic/CZlt_to.con
317 cic:/CoRN/algebra/CLogic/CZ_exh.con
318 cic:/CoRN/algebra/CLogic/CTrue_rect.con
319 cic:/CoRN/algebra/CLogic/CTrue_rec.con
320 cic:/CoRN/algebra/CLogic/CTrue_ind.con
321 cic:/CoRN/algebra/CLogic/CTrue.ind
322 cic:/CoRN/algebra/CLogic/CProp.con
323 cic:/CoRN/algebra/CLogic/COr_rect.con
324 cic:/CoRN/algebra/CLogic/COr_rec.con
325 cic:/CoRN/algebra/CLogic/COr_ind.con
326 cic:/CoRN/algebra/CLogic/COr.ind
327 cic:/CoRN/algebra/CLogic/CNot_Not_or.con
328 cic:/CoRN/algebra/CLogic/CNot.con
329 cic:/CoRN/algebra/CLogic/CFalse_rect.con
330 cic:/CoRN/algebra/CLogic/CFalse_rec.con
331 cic:/CoRN/algebra/CLogic/CFalse_ind.con
332 cic:/CoRN/algebra/CLogic/CFalse.ind
333 cic:/CoRN/algebra/CLogic/CAnd_rect.con
334 cic:/CoRN/algebra/CLogic/CAnd_rec.con
335 cic:/CoRN/algebra/CLogic/CAnd_proj2.con
336 cic:/CoRN/algebra/CLogic/CAnd_proj1.con
337 cic:/CoRN/algebra/CLogic/CAnd_ind.con
338 cic:/CoRN/algebra/CLogic/CAnd.ind
339 cic:/CoRN/algebra/CModule_Homomorphisms/mh_strext.con
340 cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_zero.con
341 cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_unit.con
342 cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_plus.con
343 cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_mult.con
344 cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_minus.con
345 cic:/CoRN/algebra/CModule_Homomorphisms/mh_apzero.con
346 cic:/CoRN/algebra/CModule_Homomorphisms/hommap.con
347 cic:/CoRN/algebra/CModule_Homomorphisms/hom3.con
348 cic:/CoRN/algebra/CModule_Homomorphisms/hom2.con
349 cic:/CoRN/algebra/CModule_Homomorphisms/hom1.con
350 cic:/CoRN/algebra/CModule_Homomorphisms/fun_pres_unit.con
351 cic:/CoRN/algebra/CModule_Homomorphisms/fun_pres_plus.con
352 cic:/CoRN/algebra/CModule_Homomorphisms/fun_pres_mult.con
353 cic:/CoRN/algebra/CModule_Homomorphisms/ModHom_rect.con
354 cic:/CoRN/algebra/CModule_Homomorphisms/ModHom_rec.con
355 cic:/CoRN/algebra/CModule_Homomorphisms/ModHom_ind.con
356 cic:/CoRN/algebra/CModule_Homomorphisms/ModHom.ind
357 cic:/CoRN/algebra/CModules/submod_rect.con
358 cic:/CoRN/algebra/CModules/submod_rec.con
359 cic:/CoRN/algebra/CModules/submod_is_submod.con
360 cic:/CoRN/algebra/CModules/submod_ind.con
361 cic:/CoRN/algebra/CModules/submod_as_CSetoid.con
362 cic:/CoRN/algebra/CModules/submod.ind
363 cic:/CoRN/algebra/CModules/smzero.con
364 cic:/CoRN/algebra/CModules/smproof.con
365 cic:/CoRN/algebra/CModules/smpred.con
366 cic:/CoRN/algebra/CModules/smplus.con
367 cic:/CoRN/algebra/CModules/smmult.con
368 cic:/CoRN/algebra/CModules/rm_proof.con
369 cic:/CoRN/algebra/CModules/rm_pl2.con
370 cic:/CoRN/algebra/CModules/rm_pl1.con
371 cic:/CoRN/algebra/CModules/rm_one.con
372 cic:/CoRN/algebra/CModules/rm_mult.con
373 cic:/CoRN/algebra/CModules/rm_mu.con
374 cic:/CoRN/algebra/CModules/rm_crr.con
375 cic:/CoRN/algebra/CModules/mu_zerox.con
376 cic:/CoRN/algebra/CModules/mu_strext.con
377 cic:/CoRN/algebra/CModules/mu_plus2.con
378 cic:/CoRN/algebra/CModules/mu_plus1.con
379 cic:/CoRN/algebra/CModules/mu_one.con
380 cic:/CoRN/algebra/CModules/mu_mult.con
381 cic:/CoRN/algebra/CModules/mu_minusonex.con
382 cic:/CoRN/algebra/CModules/mu_minusax.con
383 cic:/CoRN/algebra/CModules/mu_azero.con
384 cic:/CoRN/algebra/CModules/mu_axap0_xap0.con
385 cic:/CoRN/algebra/CModules/mu_axap0_aap0.con
386 cic:/CoRN/algebra/CModules/mu_aminusx.con
387 cic:/CoRN/algebra/CModules/mu0help2.con
388 cic:/CoRN/algebra/CModules/mu0help.con
389 cic:/CoRN/algebra/CModules/is_submod_rect.con
390 cic:/CoRN/algebra/CModules/is_submod_rec.con
391 cic:/CoRN/algebra/CModules/is_submod_ind.con
392 cic:/CoRN/algebra/CModules/is_submod.ind
393 cic:/CoRN/algebra/CModules/is_comod_rect.con
394 cic:/CoRN/algebra/CModules/is_comod_rec.con
395 cic:/CoRN/algebra/CModules/is_comod_ind.con
396 cic:/CoRN/algebra/CModules/is_comod.ind
397 cic:/CoRN/algebra/CModules/is_RModule_rect.con
398 cic:/CoRN/algebra/CModules/is_RModule_rec.con
399 cic:/CoRN/algebra/CModules/is_RModule_ind.con
400 cic:/CoRN/algebra/CModules/is_RModule.ind
401 cic:/CoRN/algebra/CModules/comod_wd.con
402 cic:/CoRN/algebra/CModules/comod_rect.con
403 cic:/CoRN/algebra/CModules/comod_rec.con
404 cic:/CoRN/algebra/CModules/comod_plus.con
405 cic:/CoRN/algebra/CModules/comod_nonzero.con
406 cic:/CoRN/algebra/CModules/comod_mult.con
407 cic:/CoRN/algebra/CModules/comod_is_comod.con
408 cic:/CoRN/algebra/CModules/comod_ind.con
409 cic:/CoRN/algebra/CModules/comod_as_CSetoid.con
410 cic:/CoRN/algebra/CModules/comod_apzero.con
411 cic:/CoRN/algebra/CModules/comod.ind
412 cic:/CoRN/algebra/CModules/cmproof.con
413 cic:/CoRN/algebra/CModules/cmpred.con
414 cic:/CoRN/algebra/CModules/cmplus.con
415 cic:/CoRN/algebra/CModules/cmmult.con
416 cic:/CoRN/algebra/CModules/cmapzero.con
417 cic:/CoRN/algebra/CModules/R_is_RModule.con
418 cic:/CoRN/algebra/CModules/R_as_RModule.con
419 cic:/CoRN/algebra/CModules/RModule_rect.con
420 cic:/CoRN/algebra/CModules/RModule_rec.con
421 cic:/CoRN/algebra/CModules/RModule_is_RModule.con
422 cic:/CoRN/algebra/CModules/RModule_ind.con
423 cic:/CoRN/algebra/CModules/RModule.ind
424 cic:/matita/dama/bishop_set/le_le_eq.con
425 cic:/matita/dama/bishop_set/le_antisymmetric.con
426 cic:/matita/dama/bishop_set/eq_trans_.con
427 cic:/matita/dama/bishop_set/eq_sym_.con
428 cic:/matita/dama/bishop_set/eq_sym.con
429 cic:/matita/dama/bishop_set/eq_reflexive.con
430 cic:/matita/dama/bishop_set/eq.con
431 cic:/matita/dama/bishop_set/bs_symmetric.con
432 cic:/matita/dama/bishop_set/bs_cotransitive.con
433 cic:/matita/dama/bishop_set/bs_coreflexive.con
434 cic:/matita/dama/bishop_set/bs_carr.con
435 cic:/matita/dama/bishop_set/bs_apart.con
436 cic:/matita/dama/bishop_set/bishop_set_rect.con
437 cic:/matita/dama/bishop_set/bishop_set_rec.con
438 cic:/matita/dama/bishop_set/bishop_set_of_ordered_set.con
439 cic:/matita/dama/bishop_set/bishop_set_ind.con
440 cic:/matita/dama/bishop_set/bishop_set.ind
441 cic:/matita/dama/bishop_set_rewrite/le_rewr.con
442 cic:/matita/dama/bishop_set_rewrite/le_rewl.con
443 cic:/matita/dama/bishop_set_rewrite/exc_rewr.con
444 cic:/matita/dama/bishop_set_rewrite/exc_rewl.con
445 cic:/matita/dama/bishop_set_rewrite/eq_trans.con
446 cic:/matita/dama/bishop_set_rewrite/ap_rewr.con
447 cic:/matita/dama/bishop_set_rewrite/ap_rewl.con
448 cic:/matita/dama/cprop_connectives/transitive.con
449 cic:/matita/dama/cprop_connectives/symmetric.con
450 cic:/matita/dama/cprop_connectives/reflexive.con
451 cic:/matita/dama/cprop_connectives/exT_rect.con
452 cic:/matita/dama/cprop_connectives/exT_rec.con
453 cic:/matita/dama/cprop_connectives/exT_ind.con
454 cic:/matita/dama/cprop_connectives/exT.ind
455 cic:/matita/dama/cprop_connectives/cotransitive.con
456 cic:/matita/dama/cprop_connectives/coreflexive.con
457 cic:/matita/dama/cprop_connectives/antisymmetric.con
458 cic:/matita/dama/cprop_connectives/Or_rect.con
459 cic:/matita/dama/cprop_connectives/Or_rec.con
460 cic:/matita/dama/cprop_connectives/Or_ind.con
461 cic:/matita/dama/cprop_connectives/Or.ind
462 cic:/matita/dama/cprop_connectives/Not.con
463 cic:/matita/dama/cprop_connectives/False_rect.con
464 cic:/matita/dama/cprop_connectives/False_rec.con
465 cic:/matita/dama/cprop_connectives/False_ind.con
466 cic:/matita/dama/cprop_connectives/False.ind
467 cic:/matita/dama/cprop_connectives/And_rect.con
468 cic:/matita/dama/cprop_connectives/And_rec.con
469 cic:/matita/dama/cprop_connectives/And_ind.con
470 cic:/matita/dama/cprop_connectives/And.ind
471 cic:/matita/dama/ordered_set/os_excess.con
472 cic:/matita/dama/ordered_set/os_cotransitive.con
473 cic:/matita/dama/ordered_set/os_coreflexive.con
474 cic:/matita/dama/ordered_set/os_carr.con
475 cic:/matita/dama/ordered_set/ordered_set_rect.con
476 cic:/matita/dama/ordered_set/ordered_set_rec.con
477 cic:/matita/dama/ordered_set/ordered_set_ind.con
478 cic:/matita/dama/ordered_set/ordered_set.ind
479 cic:/matita/dama/ordered_set/le_transitive.con
480 cic:/matita/dama/ordered_set/le_reflexive.con
481 cic:/matita/dama/ordered_set/le.con
482 cic:/matita/dama/ordered_set/exc_le_variance.con
483 cic:/matita/dama/sequence/sequence.con
484 cic:/matita/dama/sequence/fun_of_sequence.con
485 cic:/matita/dama/supremum/upper_bound.con
486 cic:/matita/dama/supremum/uniq_supremum.con
487 cic:/matita/dama/supremum/strong_sup.con
488 cic:/matita/dama/supremum/increasing.con
489 cic:/matita/higher_order_defs/functions/symmetric2.con
490 cic:/matita/higher_order_defs/functions/symmetric.con
491 cic:/matita/higher_order_defs/functions/surjective.con
492 cic:/matita/higher_order_defs/functions/monotonic.con
493 cic:/matita/higher_order_defs/functions/injective.con
494 cic:/matita/higher_order_defs/functions/eq_f_g_h.con
495 cic:/matita/higher_order_defs/functions/distributive2.con
496 cic:/matita/higher_order_defs/functions/distributive.con
497 cic:/matita/higher_order_defs/functions/compose.con
498 cic:/matita/higher_order_defs/functions/associative.con
499 cic:/matita/higher_order_defs/relations/transitive.con
500 cic:/matita/higher_order_defs/relations/tight_apart.con
501 cic:/matita/higher_order_defs/relations/symmetric.con
502 cic:/matita/higher_order_defs/relations/relation.con
503 cic:/matita/higher_order_defs/relations/reflexive.con
504 cic:/matita/higher_order_defs/relations/irreflexive.con
505 cic:/matita/higher_order_defs/relations/cotransitive.con
506 cic:/matita/higher_order_defs/relations/antisymmetric.con
507 cic:/matita/logic/connectives/proj2.con
508 cic:/matita/logic/connectives/proj1.con
509 cic:/matita/logic/connectives/iff.con
510 cic:/matita/logic/connectives/ex_ind.con
511 cic:/matita/logic/connectives/ex2_ind.con
512 cic:/matita/logic/connectives/ex2.ind
513 cic:/matita/logic/connectives/ex.ind
514 cic:/matita/logic/connectives/decidable.con
515 cic:/matita/logic/connectives/absurd.con
516 cic:/matita/logic/connectives/True_rect.con
517 cic:/matita/logic/connectives/True_rec.con
518 cic:/matita/logic/connectives/True_ind.con
519 cic:/matita/logic/connectives/True.ind
520 cic:/matita/logic/connectives/Or_ind.con
521 cic:/matita/logic/connectives/Or_ind'.con
522 cic:/matita/logic/connectives/Or.ind
523 cic:/matita/logic/connectives/Not.con
524 cic:/matita/logic/connectives/False_rect.con
525 cic:/matita/logic/connectives/False_rec.con
526 cic:/matita/logic/connectives/False_ind.con
527 cic:/matita/logic/connectives/False.ind
528 cic:/matita/logic/connectives/And_rect.con
529 cic:/matita/logic/connectives/And_rec.con
530 cic:/matita/logic/connectives/And_ind.con
531 cic:/matita/logic/connectives/And.ind
532 cic:/matita/logic/equality/transitive_eq.con
533 cic:/matita/logic/equality/trans_sym_eq.con
534 cic:/matita/logic/equality/trans_eq.con
535 cic:/matita/logic/equality/symmetric_eq.con
536 cic:/matita/logic/equality/sym_eq.con
537 cic:/matita/logic/equality/reflexive_eq.con
538 cic:/matita/logic/equality/nu_left_inv.con
539 cic:/matita/logic/equality/nu_inv.con
540 cic:/matita/logic/equality/nu_constant.con
541 cic:/matita/logic/equality/nu.con
542 cic:/matita/logic/equality/eq_to_eq_to_eq_p_q.con
543 cic:/matita/logic/equality/eq_rect.con
544 cic:/matita/logic/equality/eq_rect'.con
545 cic:/matita/logic/equality/eq_rec.con
546 cic:/matita/logic/equality/eq_ind.con
547 cic:/matita/logic/equality/eq_f2.con
548 cic:/matita/logic/equality/eq_f.con
549 cic:/matita/logic/equality/eq_f'.con
550 cic:/matita/logic/equality/eq_elim_r.con
551 cic:/matita/logic/equality/eq_elim_r'.con
552 cic:/matita/logic/equality/eq_elim_r''.con
553 cic:/matita/logic/equality/eq_OF_eq2.con
554 cic:/matita/logic/equality/eq_OF_eq1.con
555 cic:/matita/logic/equality/eq_OF_eq.con
556 cic:/matita/logic/equality/eq.ind
557 cic:/matita/logic/equality/comp.con
558 cic:/matita/nat/nat/pred_Sn.con
559 cic:/matita/nat/nat/pred.con
560 cic:/matita/nat/nat/not_zero.con
561 cic:/matita/nat/nat/not_eq_n_Sn.con
562 cic:/matita/nat/nat/not_eq_S.con
563 cic:/matita/nat/nat/not_eq_O_S.con
564 cic:/matita/nat/nat/nat_rect.con
565 cic:/matita/nat/nat/nat_rec.con
566 cic:/matita/nat/nat/nat_ind.con
567 cic:/matita/nat/nat/nat_elim2.con
568 cic:/matita/nat/nat/nat_case1.con
569 cic:/matita/nat/nat/nat_case.con
570 cic:/matita/nat/nat/nat.ind
571 cic:/matita/nat/nat/injective_S.con
572 cic:/matita/nat/nat/inj_S.con
573 cic:/matita/nat/nat/decidable_eq_nat.con
projects / helm.git / blob