1 cic:/matita/nat/compare/not_eq_to_eqb_false.con
2 cic:/matita/nat/compare/nat_compare_to_Prop.con
3 cic:/matita/nat/compare/nat_compare_pred_pred.con
4 cic:/matita/nat/compare/nat_compare_n_n.con
5 cic:/matita/nat/compare/nat_compare_n_m_m_n.con
6 cic:/matita/nat/compare/nat_compare_elim.con
7 cic:/matita/nat/compare/nat_compare_S_S.con
8 cic:/matita/nat/compare/nat_compare.con
9 cic:/matita/nat/compare/ltb_to_Prop.con
10 cic:/matita/nat/compare/ltb_elim.con
11 cic:/matita/nat/compare/ltb.con
12 cic:/matita/nat/compare/lt_to_leb_false.con
13 cic:/matita/nat/compare/leb_true_to_le.con
14 cic:/matita/nat/compare/leb_to_Prop.con
15 cic:/matita/nat/compare/leb_false_to_not_le.con
16 cic:/matita/nat/compare/leb_elim.con
17 cic:/matita/nat/compare/leb_demod3.con
18 cic:/matita/nat/compare/leb_demod2.con
19 cic:/matita/nat/compare/leb_demod1.con
20 cic:/matita/nat/compare/leb.con
21 cic:/matita/nat/compare/le_to_leb_true.con
22 cic:/matita/nat/compare/eqb_true_to_eq.con
23 cic:/matita/nat/compare/eqb_to_Prop.con
24 cic:/matita/nat/compare/eqb_n_n.con
25 cic:/matita/nat/compare/eqb_false_to_not_eq.con
26 cic:/matita/nat/compare/eqb_elim.con
27 cic:/matita/nat/compare/eqb.con
28 cic:/matita/nat/compare/eq_to_eqb_true.con
29 cic:/matita/nat/compare/compare_demod2.con
30 cic:/matita/nat/compare/compare_demod1.con
31 cic:/matita/nat/nat/pred_demod2.con
32 cic:/matita/nat/nat/pred_demod1.con
33 cic:/matita/nat/nat/pred_Sn.con
34 cic:/matita/nat/nat/pred.con
35 cic:/matita/nat/nat/not_zero.con
36 cic:/matita/nat/nat/not_eq_n_Sn.con
37 cic:/matita/nat/nat/not_eq_S.con
38 cic:/matita/nat/nat/not_eq_O_S.con
39 cic:/matita/nat/nat/nat_rect.con
40 cic:/matita/nat/nat/nat_rec.con
41 cic:/matita/nat/nat/nat_ind.con
42 cic:/matita/nat/nat/nat_elim2.con
43 cic:/matita/nat/nat/nat_case1.con
44 cic:/matita/nat/nat/nat_case.con
45 cic:/matita/nat/nat/nat.ind
46 cic:/matita/nat/nat/injective_S.con
47 cic:/matita/nat/nat/inj_S.con
48 cic:/matita/nat/nat/decidable_eq_nat.con
49 cic:/matita/nat/orders/transitive_lt.con
50 cic:/matita/nat/orders/transitive_le.con
51 cic:/matita/nat/orders/trans_lt.con
52 cic:/matita/nat/orders/trans_le.con
53 cic:/matita/nat/orders/not_lt_to_le.con
54 cic:/matita/nat/orders/not_le_to_lt.con
55 cic:/matita/nat/orders/not_le_Sn_n.con
56 cic:/matita/nat/orders/not_le_Sn_O.con
57 cic:/matita/nat/orders/not_eq_to_le_to_lt.con
58 cic:/matita/nat/orders/nat_elim1.con
59 cic:/matita/nat/orders/ltn_to_ltO.con
60 cic:/matita/nat/orders/lt_to_not_le.con
61 cic:/matita/nat/orders/lt_to_not_eq.con
62 cic:/matita/nat/orders/lt_to_lt_S_S.con
63 cic:/matita/nat/orders/lt_to_le_to_lt.con
64 cic:/matita/nat/orders/lt_to_le.con
65 cic:/matita/nat/orders/lt_pred.con
66 cic:/matita/nat/orders/lt_n_m_to_not_lt_m_Sn.con
67 cic:/matita/nat/orders/lt_S_to_lt.con
68 cic:/matita/nat/orders/lt_S_to_le.con
69 cic:/matita/nat/orders/lt_S_S_to_lt.con
70 cic:/matita/nat/orders/lt_SO_n_to_lt_O_pred_n.con
71 cic:/matita/nat/orders/lt_O_n_elim.con
72 cic:/matita/nat/orders/lt_O_S.con
73 cic:/matita/nat/orders/lt.con
74 cic:/matita/nat/orders/le_to_or_lt_eq.con
75 cic:/matita/nat/orders/le_to_not_lt.con
76 cic:/matita/nat/orders/le_to_lt_to_lt.con
77 cic:/matita/nat/orders/le_to_le_to_eq.con
78 cic:/matita/nat/orders/le_to_le_pred.con
79 cic:/matita/nat/orders/le_pred_to_le.con
80 cic:/matita/nat/orders/le_pred_n.con
81 cic:/matita/nat/orders/le_n_m_to_lt_m_Sn_to_eq_n_m.con
82 cic:/matita/nat/orders/le_n_fn.con
83 cic:/matita/nat/orders/le_n_Sn.con
84 cic:/matita/nat/orders/le_n_Sm_elim.con
85 cic:/matita/nat/orders/le_n_O_to_eq.con
86 cic:/matita/nat/orders/le_n_O_elim.con
87 cic:/matita/nat/orders/le_inv.con
88 cic:/matita/nat/orders/le_ind.con
89 cic:/matita/nat/orders/le_S_S_to_le.con
90 cic:/matita/nat/orders/le_S_S.con
91 cic:/matita/nat/orders/le_O_n.con
92 cic:/matita/nat/orders/leS_to_not_zero.con
93 cic:/matita/nat/orders/le.ind
94 cic:/matita/nat/orders/increasing_to_monotonic.con
95 cic:/matita/nat/orders/increasing_to_le2.con
96 cic:/matita/nat/orders/increasing_to_le.con
97 cic:/matita/nat/orders/increasing.con
98 cic:/matita/nat/orders/gt.con
99 cic:/matita/nat/orders/ge.con
100 cic:/matita/nat/orders/eq_to_not_lt.con
101 cic:/matita/nat/orders/decidable_lt.con
102 cic:/matita/nat/orders/decidable_le.con
103 cic:/matita/nat/orders/antisymmetric_le.con
104 cic:/matita/nat/orders/antisym_le.con
105 cic:/matita/nat/orders/S_pred.con
106 cic:/matita/nat/orders/Not_lt_n_n.con
107 cic:/matita/nat/plus/sym_plus.con
108 cic:/matita/nat/plus/plus_n_Sm.con
109 cic:/matita/nat/plus/plus_n_SO.con
110 cic:/matita/nat/plus/plus_n_O.con
111 cic:/matita/nat/plus/plus_demod4.con
112 cic:/matita/nat/plus/plus_demod3.con
113 cic:/matita/nat/plus/plus_demod2.con
114 cic:/matita/nat/plus/plus_demod1.con
115 cic:/matita/nat/plus/plus.con
116 cic:/matita/nat/plus/injective_plus_r.con
117 cic:/matita/nat/plus/injective_plus_l.con
118 cic:/matita/nat/plus/inj_plus_r.con
119 cic:/matita/nat/plus/inj_plus_l.con
120 cic:/matita/nat/plus/associative_plus.con
121 cic:/matita/nat/plus/assoc_plus.con
122 cic:/matita/nat/times/times_n_Sm.con
123 cic:/matita/nat/times/times_n_SO.con
124 cic:/matita/nat/times/times_n_O.con
125 cic:/matita/nat/times/times_demod6.con
126 cic:/matita/nat/times/times_demod4.con
127 cic:/matita/nat/times/times_demod2.con
128 cic:/matita/nat/times/times_demod1.con
129 cic:/matita/nat/times/times_SSO_n.con
130 cic:/matita/nat/times/times_SSO.con
131 cic:/matita/nat/times/times_O_to_O.con
132 cic:/matita/nat/times/times.con
133 cic:/matita/nat/times/symmetric_times.con
134 cic:/matita/nat/times/sym_times.con
135 cic:/matita/nat/times/or_eq_eq_S.con
136 cic:/matita/nat/times/distributive_times_plus.con
137 cic:/matita/nat/times/distr_times_plus.con
138 cic:/matita/nat/times/associative_times.con
139 cic:/matita/nat/times/assoc_times.con
140 cic:/matita/Z/z/pos_n_eq_S_n.con
141 cic:/matita/Z/z/not_eq_pos_neg.con
142 cic:/matita/Z/z/not_eq_OZ_pos.con
143 cic:/matita/Z/z/not_eq_OZ_neg.con
144 cic:/matita/Z/z/neg_Z_of_nat.con
145 cic:/matita/Z/z/injective_pos.con
146 cic:/matita/Z/z/injective_neg.con
147 cic:/matita/Z/z/inj_pos.con
148 cic:/matita/Z/z/inj_neg.con
149 cic:/matita/Z/z/decidable_eq_Z.con
150 cic:/matita/Z/z/abs.con
151 cic:/matita/Z/z/Zsucc_Zpred.con
152 cic:/matita/Z/z/Zsucc.con
153 cic:/matita/Z/z/Zpred_Zsucc.con
154 cic:/matita/Z/z/Zpred.con
155 cic:/matita/Z/z/Z_rect.con
156 cic:/matita/Z/z/Z_rec.con
157 cic:/matita/Z/z/Z_of_nat.con
158 cic:/matita/Z/z/Z_ind.con
159 cic:/matita/Z/z/Z.ind
160 cic:/matita/Z/z/OZ_test_to_Prop.con
161 cic:/matita/Z/z/OZ_test.con
162 cic:/matita/algebra/monoids/premonoid.con
163 cic:/matita/algebra/monoids/monoid_properties.con
164 cic:/matita/algebra/monoids/magma.con
165 cic:/matita/algebra/monoids/is_semi_group.con
166 cic:/matita/algebra/monoids/is_right_inverse.con
167 cic:/matita/algebra/monoids/is_left_inverse_to_is_right_inverse_to_eq.con
168 cic:/matita/algebra/monoids/is_left_inverse.con
169 cic:/matita/algebra/monoids/isSemiGroup_OF_Monoid.con
170 cic:/matita/algebra/monoids/isMonoid_rect.con
171 cic:/matita/algebra/monoids/isMonoid_rec.con
172 cic:/matita/algebra/monoids/isMonoid_ind.con
173 cic:/matita/algebra/monoids/isMonoid.ind
174 cic:/matita/algebra/monoids/e_is_right_unit.con
175 cic:/matita/algebra/monoids/e_is_left_unit.con
176 cic:/matita/algebra/monoids/e.con
177 cic:/matita/algebra/monoids/Type_OF_PreMonoid.con
178 cic:/matita/algebra/monoids/Type_OF_Monoid.con
179 cic:/matita/algebra/monoids/PreMonoid_rect.con
180 cic:/matita/algebra/monoids/PreMonoid_rec.con
181 cic:/matita/algebra/monoids/PreMonoid_ind.con
182 cic:/matita/algebra/monoids/PreMonoid.ind
183 cic:/matita/algebra/monoids/Monoid_rect.con
184 cic:/matita/algebra/monoids/Monoid_rec.con
185 cic:/matita/algebra/monoids/Monoid_ind.con
186 cic:/matita/algebra/monoids/Monoid.ind
187 cic:/matita/algebra/monoids/Magma_OF_Monoid.con
188 cic:/matita/algebra/semigroups/semigroup_properties.con
189 cic:/matita/algebra/semigroups/op_associative.con
190 cic:/matita/algebra/semigroups/op.con
191 cic:/matita/algebra/semigroups/magma.con
192 cic:/matita/algebra/semigroups/is_right_unit.con
193 cic:/matita/algebra/semigroups/is_left_unit_to_is_right_unit_to_eq.con
194 cic:/matita/algebra/semigroups/is_left_unit.con
195 cic:/matita/algebra/semigroups/isSemiGroup_rect.con
196 cic:/matita/algebra/semigroups/isSemiGroup_rec.con
197 cic:/matita/algebra/semigroups/isSemiGroup_ind.con
198 cic:/matita/algebra/semigroups/isSemiGroup.ind
199 cic:/matita/algebra/semigroups/carrier.con
200 cic:/matita/algebra/semigroups/Type_OF_SemiGroup.con
201 cic:/matita/algebra/semigroups/SemiGroup_rect.con
202 cic:/matita/algebra/semigroups/SemiGroup_rec.con
203 cic:/matita/algebra/semigroups/SemiGroup_ind.con
204 cic:/matita/algebra/semigroups/SemiGroup.ind
205 cic:/matita/algebra/semigroups/Magma_rect.con
206 cic:/matita/algebra/semigroups/Magma_rec.con
207 cic:/matita/algebra/semigroups/Magma_ind.con
208 cic:/matita/algebra/semigroups/Magma.ind
209 cic:/matita/datatypes/bool/true_to_true_to_andb_true.con
210 cic:/matita/datatypes/bool/orb_sym.con
211 cic:/matita/datatypes/bool/orb_elim.con
212 cic:/matita/datatypes/bool/orb.con
213 cic:/matita/datatypes/bool/notb_notb.con
214 cic:/matita/datatypes/bool/notb_elim.con
215 cic:/matita/datatypes/bool/notb.con
216 cic:/matita/datatypes/bool/not_eq_true_false.con
217 cic:/matita/datatypes/bool/injective_notb.con
218 cic:/matita/datatypes/bool/if_then_else.con
219 cic:/matita/datatypes/bool/bool_to_decidable_eq.con
220 cic:/matita/datatypes/bool/bool_rect.con
221 cic:/matita/datatypes/bool/bool_rec.con
222 cic:/matita/datatypes/bool/bool_ind.con
223 cic:/matita/datatypes/bool/bool_elim.con
224 cic:/matita/datatypes/bool/bool.ind
225 cic:/matita/datatypes/bool/andb_true_true_r.con
226 cic:/matita/datatypes/bool/andb_true_true.con
227 cic:/matita/datatypes/bool/andb_sym.con
228 cic:/matita/datatypes/bool/andb_elim.con
229 cic:/matita/datatypes/bool/andb_assoc.con
230 cic:/matita/datatypes/bool/andb.con
231 cic:/matita/datatypes/bool/and_true.con
232 cic:/matita/datatypes/bool/P_x_to_P_x_to_eq.con
233 cic:/matita/datatypes/compare/compare_rect.con
234 cic:/matita/datatypes/compare/compare_rec.con
235 cic:/matita/datatypes/compare/compare_invert.con
236 cic:/matita/datatypes/compare/compare_ind.con
237 cic:/matita/datatypes/compare/compare.ind
238 cic:/matita/datatypes/constructors/void_rect.con
239 cic:/matita/datatypes/constructors/void_rec.con
240 cic:/matita/datatypes/constructors/void_ind.con
241 cic:/matita/datatypes/constructors/void.ind
242 cic:/matita/datatypes/constructors/unit_rect.con
243 cic:/matita/datatypes/constructors/unit_rec.con
244 cic:/matita/datatypes/constructors/unit_ind.con
245 cic:/matita/datatypes/constructors/unit.ind
246 cic:/matita/datatypes/constructors/snd.con
247 cic:/matita/datatypes/constructors/option_rect.con
248 cic:/matita/datatypes/constructors/option_rec.con
249 cic:/matita/datatypes/constructors/option_ind.con
250 cic:/matita/datatypes/constructors/option.ind
251 cic:/matita/datatypes/constructors/fst.con
252 cic:/matita/datatypes/constructors/eq_pair_fst_snd.con
253 cic:/matita/datatypes/constructors/Sum_rect.con
254 cic:/matita/datatypes/constructors/Sum_rec.con
255 cic:/matita/datatypes/constructors/Sum_ind.con
256 cic:/matita/datatypes/constructors/Sum.ind
257 cic:/matita/datatypes/constructors/Prod_rect.con
258 cic:/matita/datatypes/constructors/Prod_rec.con
259 cic:/matita/datatypes/constructors/Prod_ind.con
260 cic:/matita/datatypes/constructors/Prod.ind
261 cic:/matita/decidable_kit/decidable/reflect_rect.con
262 cic:/matita/decidable_kit/decidable/reflect_rec.con
263 cic:/matita/decidable_kit/decidable/reflect_inv.con
264 cic:/matita/decidable_kit/decidable/reflect_ind.con
265 cic:/matita/decidable_kit/decidable/reflect.ind
266 cic:/matita/decidable_kit/decidable/prove_reflect.con
267 cic:/matita/decidable_kit/decidable/p2bT.con
268 cic:/matita/decidable_kit/decidable/p2bF.con
269 cic:/matita/decidable_kit/decidable/orbP.con
270 cic:/matita/decidable_kit/decidable/orbC.con
271 cic:/matita/decidable_kit/decidable/orb.con
272 cic:/matita/decidable_kit/decidable/negbP.con
273 cic:/matita/decidable_kit/decidable/negb.con
274 cic:/matita/decidable_kit/decidable/ltb_refl.con
275 cic:/matita/decidable_kit/decidable/ltb_n_Sm.con
276 cic:/matita/decidable_kit/decidable/ltbW.con
277 cic:/matita/decidable_kit/decidable/ltbP.con
278 cic:/matita/decidable_kit/decidable/ltb.con
279 cic:/matita/decidable_kit/decidable/ltW.con
280 cic:/matita/decidable_kit/decidable/ltS.con
281 cic:/matita/decidable_kit/decidable/ltS'.con
282 cic:/matita/decidable_kit/decidable/leb_refl.con
283 cic:/matita/decidable_kit/decidable/leb_eqb.con
284 cic:/matita/decidable_kit/decidable/lebW.con
285 cic:/matita/decidable_kit/decidable/lebP.con
286 cic:/matita/decidable_kit/decidable/idP.con
287 cic:/matita/decidable_kit/decidable/eq_to_bool.con
288 cic:/matita/decidable_kit/decidable/congr_S.con
289 cic:/matita/decidable_kit/decidable/bool_to_eq.con
290 cic:/matita/decidable_kit/decidable/b2pT.con
291 cic:/matita/decidable_kit/decidable/b2pF.con
292 cic:/matita/decidable_kit/decidable/andbPF.con
293 cic:/matita/decidable_kit/decidable/andbP.con
294 cic:/matita/decidable_kit/decidable/andb.con
295 cic:/matita/decidable_kit/eqtype/test_canonical_option_eqType.con
296 cic:/matita/decidable_kit/eqtype/sval.con
297 cic:/matita/decidable_kit/eqtype/sub_eqType.con
298 cic:/matita/decidable_kit/eqtype/sprop.con
299 cic:/matita/decidable_kit/eqtype/sort_OF_nat.con
300 cic:/matita/decidable_kit/eqtype/sort_OF_bool.con
301 cic:/matita/decidable_kit/eqtype/sort.con
302 cic:/matita/decidable_kit/eqtype/sigma_rect.con
303 cic:/matita/decidable_kit/eqtype/sigma_rec.con
304 cic:/matita/decidable_kit/eqtype/sigma_ind.con
305 cic:/matita/decidable_kit/eqtype/sigma_eq_dec.con
306 cic:/matita/decidable_kit/eqtype/sigma.ind
307 cic:/matita/decidable_kit/eqtype/option_eqType.con
308 cic:/matita/decidable_kit/eqtype/option_canonical_eqType.con
309 cic:/matita/decidable_kit/eqtype/ocmpP.con
310 cic:/matita/decidable_kit/eqtype/ocmp.con
311 cic:/matita/decidable_kit/eqtype/nat_eqType.con
312 cic:/matita/decidable_kit/eqtype/nat_canonical_eqType.con
313 cic:/matita/decidable_kit/eqtype/in_sub_rect.con
314 cic:/matita/decidable_kit/eqtype/in_sub_rec.con
315 cic:/matita/decidable_kit/eqtype/in_sub_inv.con
316 cic:/matita/decidable_kit/eqtype/in_sub_ind.con
317 cic:/matita/decidable_kit/eqtype/in_sub_eq.con
318 cic:/matita/decidable_kit/eqtype/in_sub.ind
319 cic:/matita/decidable_kit/eqtype/if_p.con
320 cic:/matita/decidable_kit/eqtype/eqbP.con
321 cic:/matita/decidable_kit/eqtype/eq_compatible.con
322 cic:/matita/decidable_kit/eqtype/eqType_rect.con
323 cic:/matita/decidable_kit/eqtype/eqType_rec.con
324 cic:/matita/decidable_kit/eqtype/eqType_ind.con
325 cic:/matita/decidable_kit/eqtype/eqType_decidable.con
326 cic:/matita/decidable_kit/eqtype/eqType.ind
327 cic:/matita/decidable_kit/eqtype/eqP.con
328 cic:/matita/decidable_kit/eqtype/cmp_refl.con
329 cic:/matita/decidable_kit/eqtype/cmpP.con
330 cic:/matita/decidable_kit/eqtype/cmpC.con
331 cic:/matita/decidable_kit/eqtype/cmp.con
332 cic:/matita/decidable_kit/eqtype/bool_eqType.con
333 cic:/matita/decidable_kit/eqtype/bool_canonical_eqType.con
334 cic:/matita/decidable_kit/eqtype/bcmpP.con
335 cic:/matita/decidable_kit/eqtype/bcmp.con
336 cic:/matita/decidable_kit/list_aux/mem.con
337 cic:/matita/decidable_kit/list_aux/list_eqType.con
338 cic:/matita/decidable_kit/list_aux/lcmp_length.con
339 cic:/matita/decidable_kit/list_aux/lcmpP.con
340 cic:/matita/decidable_kit/list_aux/lcmp.con
341 cic:/matita/decidable_kit/list_aux/count.con
342 cic:/matita/decidable_kit/streicher/stepH.con
343 cic:/matita/decidable_kit/streicher/step.con
344 cic:/matita/decidable_kit/streicher/pirrel.con
345 cic:/matita/decidable_kit/streicher/nu_k.con
346 cic:/matita/decidable_kit/streicher/nu_inv.con
347 cic:/matita/decidable_kit/streicher/nu.con
348 cic:/matita/decidable_kit/streicher/decT.con
349 cic:/matita/decidable_kit/streicher/cancel_nu_nu_inv.con
350 cic:/matita/decidable_kit/streicher/cancel.con
351 cic:/matita/demo/realisability/type_OF_SP.con
352 cic:/matita/demo/realisability/true_impl_realized.con
353 cic:/matita/demo/realisability/sigma_rect.con
354 cic:/matita/demo/realisability/sigma_rec.con
355 cic:/matita/demo/realisability/sigma_ind.con
356 cic:/matita/demo/realisability/sigma.ind
357 cic:/matita/demo/realisability/realized.con
358 cic:/matita/demo/realisability/pi2.con
359 cic:/matita/demo/realisability/pi1.con
360 cic:/matita/demo/realisability/modr.con
361 cic:/matita/demo/realisability/id_axiom.con
362 cic:/matita/demo/realisability/extraction.con
363 cic:/matita/demo/realisability/elim_abs.con
364 cic:/matita/demo/realisability/cut.con
365 cic:/matita/demo/realisability/correct2.con
366 cic:/matita/demo/realisability/correct.con
367 cic:/matita/demo/realisability/and_i.con
368 cic:/matita/demo/realisability/SP_rect.con
369 cic:/matita/demo/realisability/SP_rec.con
370 cic:/matita/demo/realisability/SP_ind.con
371 cic:/matita/demo/realisability/SP.ind
372 cic:/matita/demo/realisability/Prop_OF_SP.con
373 cic:/matita/higher_order_defs/functions/symmetric2.con
374 cic:/matita/higher_order_defs/functions/symmetric.con
375 cic:/matita/higher_order_defs/functions/surjective.con
376 cic:/matita/higher_order_defs/functions/monotonic.con
377 cic:/matita/higher_order_defs/functions/injective.con
378 cic:/matita/higher_order_defs/functions/eq_f_g_h.con
379 cic:/matita/higher_order_defs/functions/distributive2.con
380 cic:/matita/higher_order_defs/functions/distributive.con
381 cic:/matita/higher_order_defs/functions/compose.con
382 cic:/matita/higher_order_defs/functions/associative.con
383 cic:/matita/higher_order_defs/ordering/antisymmetric.con
384 cic:/matita/higher_order_defs/relations/transitive.con
385 cic:/matita/higher_order_defs/relations/tight_apart.con
386 cic:/matita/higher_order_defs/relations/symmetric.con
387 cic:/matita/higher_order_defs/relations/relation.con
388 cic:/matita/higher_order_defs/relations/reflexive.con
389 cic:/matita/higher_order_defs/relations/irreflexive.con
390 cic:/matita/higher_order_defs/relations/cotransitive.con
391 cic:/matita/higher_order_defs/relations/antisymmetric.con
392 cic:/matita/list/list/x3.con
393 cic:/matita/list/list/x2.con
394 cic:/matita/list/list/x1.con
395 cic:/matita/list/list/tmp.con
396 cic:/matita/list/list/tail_demod2.con
397 cic:/matita/list/list/tail_demod1.con
398 cic:/matita/list/list/tail.con
399 cic:/matita/list/list/permutation_inv.con
400 cic:/matita/list/list/permutation_ind.con
401 cic:/matita/list/list/permutation.ind
402 cic:/matita/list/list/permut1_inv.con
403 cic:/matita/list/list/permut1_ind.con
404 cic:/matita/list/list/nth.con
405 cic:/matita/list/list/nil_cons.con
406 cic:/matita/list/list/map_foldr2.con
407 cic:/matita/list/list/map_foldr1.con
408 cic:/matita/list/list/map_demod2.con
409 cic:/matita/list/list/map_demod1.con
410 cic:/matita/list/list/map.con
411 cic:/matita/list/list/list_rect.con
412 cic:/matita/list/list/list_rec.con
413 cic:/matita/list/list/list_ind2.con
414 cic:/matita/list/list/list_ind.con
415 cic:/matita/list/list/list.ind
416 cic:/matita/list/list/length.con
417 cic:/matita/list/list/len_demod2.con
418 cic:/matita/list/list/len_demod1.con
419 cic:/matita/list/list/le_length_filter.con
420 cic:/matita/list/list/iota_demod2.con
421 cic:/matita/list/list/iota_demod1.con
422 cic:/matita/list/list/iota.con
423 cic:/matita/list/list/id_list.con
424 cic:/matita/list/list/foldr.con
425 cic:/matita/list/list/filter_demod2.con
426 cic:/matita/list/list/filter_demod1.con
427 cic:/matita/list/list/filter.con
428 cic:/matita/list/list/eq_map.con
429 cic:/matita/list/list/cons_append_commute.con
430 cic:/matita/list/list/associative_append.con
431 cic:/matita/list/list/append_nil.con
432 cic:/matita/list/list/append_demod2.con
433 cic:/matita/list/list/append_demod1.con
434 cic:/matita/list/list/append_cons.con
435 cic:/matita/list/list/append.con
436 cic:/matita/logic/coimplication/iff_trans.con
437 cic:/matita/logic/coimplication/iff_sym.con
438 cic:/matita/logic/coimplication/iff_refl.con
439 cic:/matita/logic/coimplication/iff_intro.con
440 cic:/matita/logic/coimplication/Iff.con
441 cic:/matita/logic/connectives/proj2.con
442 cic:/matita/logic/connectives/proj1.con
443 cic:/matita/logic/connectives/iff.con
444 cic:/matita/logic/connectives/ex_ind.con
445 cic:/matita/logic/connectives/ex2_ind.con
446 cic:/matita/logic/connectives/ex2.ind
447 cic:/matita/logic/connectives/ex.ind
448 cic:/matita/logic/connectives/decidable.con
449 cic:/matita/logic/connectives/absurd.con
450 cic:/matita/logic/connectives/True_rect.con
451 cic:/matita/logic/connectives/True_rec.con
452 cic:/matita/logic/connectives/True_ind.con
453 cic:/matita/logic/connectives/True.ind
454 cic:/matita/logic/connectives/Or_ind.con
455 cic:/matita/logic/connectives/Or_ind'.con
456 cic:/matita/logic/connectives/Or.ind
457 cic:/matita/logic/connectives/Not.con
458 cic:/matita/logic/connectives/False_rect.con
459 cic:/matita/logic/connectives/False_rec.con
460 cic:/matita/logic/connectives/False_ind.con
461 cic:/matita/logic/connectives/False.ind
462 cic:/matita/logic/connectives/And_rect.con
463 cic:/matita/logic/connectives/And_rec.con
464 cic:/matita/logic/connectives/And_ind.con
465 cic:/matita/logic/connectives/And.ind
466 cic:/matita/logic/connectives2/transitive_iff.con
467 cic:/matita/logic/connectives2/symmetric_iff.con
468 cic:/matita/logic/connectives2/reflexive_iff.con
469 cic:/matita/logic/equality/transitive_eq.con
470 cic:/matita/logic/equality/trans_sym_eq.con
471 cic:/matita/logic/equality/trans_eq.con
472 cic:/matita/logic/equality/symmetric_eq.con
473 cic:/matita/logic/equality/sym_eq.con
474 cic:/matita/logic/equality/reflexive_eq.con
475 cic:/matita/logic/equality/nu_left_inv.con
476 cic:/matita/logic/equality/nu_inv.con
477 cic:/matita/logic/equality/nu_constant.con
478 cic:/matita/logic/equality/nu.con
479 cic:/matita/logic/equality/eq_to_eq_to_eq_p_q.con
480 cic:/matita/logic/equality/eq_rect.con
481 cic:/matita/logic/equality/eq_rect'.con
482 cic:/matita/logic/equality/eq_rec.con
483 cic:/matita/logic/equality/eq_ind.con
484 cic:/matita/logic/equality/eq_f2.con
485 cic:/matita/logic/equality/eq_f.con
486 cic:/matita/logic/equality/eq_f'.con
487 cic:/matita/logic/equality/eq_elim_r.con
488 cic:/matita/logic/equality/eq_elim_r'.con
489 cic:/matita/logic/equality/eq_elim_r''.con
490 cic:/matita/logic/equality/eq_OF_eq2.con
491 cic:/matita/logic/equality/eq_OF_eq1.con
492 cic:/matita/logic/equality/eq_OF_eq.con
493 cic:/matita/logic/equality/eq.ind
494 cic:/matita/logic/equality/comp.con
495 cic:/matita/technicalities/setoids/variance_rect.con
496 cic:/matita/technicalities/setoids/variance_rec.con
497 cic:/matita/technicalities/setoids/variance_of_argument_class.con
498 cic:/matita/technicalities/setoids/variance_ind.con
499 cic:/matita/technicalities/setoids/variance.ind
500 cic:/matita/technicalities/setoids/rewrite_direction_rect.con
501 cic:/matita/technicalities/setoids/rewrite_direction_rec.con
502 cic:/matita/technicalities/setoids/rewrite_direction_ind.con
503 cic:/matita/technicalities/setoids/rewrite_direction.ind
504 cic:/matita/technicalities/setoids/relation_of_relation_class.con
505 cic:/matita/technicalities/setoids/relation_of_product_of_arguments.con
506 cic:/matita/technicalities/setoids/relation_of_areflexive_relation_class.con
507 cic:/matita/technicalities/setoids/relation_class_of_reflexive_relation_class.con
508 cic:/matita/technicalities/setoids/relation_class_of_argument_class.con
509 cic:/matita/technicalities/setoids/relation_class_of_areflexive_relation_class.con
510 cic:/matita/technicalities/setoids/product_of_arguments.con
511 cic:/matita/technicalities/setoids/opposite_direction_idempotent.con
512 cic:/matita/technicalities/setoids/opposite_direction.con
513 cic:/matita/technicalities/setoids/nelistT_rect.con
514 cic:/matita/technicalities/setoids/nelistT_rec.con
515 cic:/matita/technicalities/setoids/nelistT_ind.con
516 cic:/matita/technicalities/setoids/nelistT.ind
517 cic:/matita/technicalities/setoids/morphism_theory_of_predicate.con
518 cic:/matita/technicalities/setoids/morphism_theory_of_function.con
519 cic:/matita/technicalities/setoids/make_compatibility_goal_aux.con
520 cic:/matita/technicalities/setoids/make_compatibility_goal.con
521 cic:/matita/technicalities/setoids/list_of_Leibniz_of_list_of_types.con
522 cic:/matita/technicalities/setoids/interp_relation_class_list.con
523 cic:/matita/technicalities/setoids/interp.con
524 cic:/matita/technicalities/setoids/impl_trans.con
525 cic:/matita/technicalities/setoids/impl_refl.con
526 cic:/matita/technicalities/setoids/impl.con
527 cic:/matita/technicalities/setoids/get_rewrite_direction.con
528 cic:/matita/technicalities/setoids/function_type_of_morphism_signature.con
529 cic:/matita/technicalities/setoids/equality_morphism_of_symmetric_reflexive_transitive_relation.con
530 cic:/matita/technicalities/setoids/equality_morphism_of_symmetric_areflexive_transitive_relation.con
531 cic:/matita/technicalities/setoids/equality_morphism_of_asymmetric_reflexive_transitive_relation.con
532 cic:/matita/technicalities/setoids/equality_morphism_of_asymmetric_areflexive_transitive_relation.con
533 cic:/matita/technicalities/setoids/directed_relation_of_relation_class.con
534 cic:/matita/technicalities/setoids/directed_relation_of_argument_class.con
535 cic:/matita/technicalities/setoids/check_if_variance_is_respected_inv.con
536 cic:/matita/technicalities/setoids/check_if_variance_is_respected_ind.con
537 cic:/matita/technicalities/setoids/check_if_variance_is_respected.ind
538 cic:/matita/technicalities/setoids/carrier_of_relation_class.con
539 cic:/matita/technicalities/setoids/carrier_of_reflexive_relation_class.con
540 cic:/matita/technicalities/setoids/carrier_of_areflexive_relation_class.con
541 cic:/matita/technicalities/setoids/apply_morphism_compatibility_Right2Left.con
542 cic:/matita/technicalities/setoids/apply_morphism_compatibility_Left2Right.con
543 cic:/matita/technicalities/setoids/apply_morphism.con
544 cic:/matita/technicalities/setoids/about_carrier_of_relation_class_and_relation_class_of_argument_class.con
545 cic:/matita/technicalities/setoids/X_Relation_Class_rect.con
546 cic:/matita/technicalities/setoids/X_Relation_Class_rec.con
547 cic:/matita/technicalities/setoids/X_Relation_Class_ind.con
548 cic:/matita/technicalities/setoids/X_Relation_Class.ind
549 cic:/matita/technicalities/setoids/Relation_Class.con
550 cic:/matita/technicalities/setoids/Reflexive_Relation_Class_rect.con
551 cic:/matita/technicalities/setoids/Reflexive_Relation_Class_rec.con
552 cic:/matita/technicalities/setoids/Reflexive_Relation_Class_ind.con
553 cic:/matita/technicalities/setoids/Reflexive_Relation_Class.ind
554 cic:/matita/technicalities/setoids/Morphism_Theory_rect.con
555 cic:/matita/technicalities/setoids/Morphism_Theory_rec.con
556 cic:/matita/technicalities/setoids/Morphism_Theory_ind.con
557 cic:/matita/technicalities/setoids/Morphism_Theory.ind
558 cic:/matita/technicalities/setoids/Morphism_Context_rect2.con
559 cic:/matita/technicalities/setoids/Morphism_Context_rect.con
560 cic:/matita/technicalities/setoids/Morphism_Context_rec.con
561 cic:/matita/technicalities/setoids/Morphism_Context_inv.con
562 cic:/matita/technicalities/setoids/Morphism_Context_ind.con
563 cic:/matita/technicalities/setoids/Morphism_Context_List_rect2.con
564 cic:/matita/technicalities/setoids/Morphism_Context_List_rect.con
565 cic:/matita/technicalities/setoids/Morphism_Context_List_rec.con
566 cic:/matita/technicalities/setoids/Morphism_Context_List_inv.con
567 cic:/matita/technicalities/setoids/Morphism_Context_List_ind.con
568 cic:/matita/technicalities/setoids/Morphism_Context.ind
569 cic:/matita/technicalities/setoids/Impl_Relation_Class.con
570 cic:/matita/technicalities/setoids/Iff_Relation_Class.con
571 cic:/matita/technicalities/setoids/Function.con
572 cic:/matita/technicalities/setoids/Compat.con
573 cic:/matita/technicalities/setoids/Arguments.con
574 cic:/matita/technicalities/setoids/Argument_Class.con
575 cic:/matita/technicalities/setoids/Areflexive_Relation_Class_rect.con
576 cic:/matita/technicalities/setoids/Areflexive_Relation_Class_rec.con
577 cic:/matita/technicalities/setoids/Areflexive_Relation_Class_ind.con
578 cic:/matita/technicalities/setoids/Areflexive_Relation_Class.ind
579 cic:/matita/tests/XXX.ind
projects / helm.git / blob