]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/depends
restructuring
[helm.git] / matita / matita / tests / depends
1 TPTP/Veloci/GRP595-1.p.ma logic/equality.ma
2 TPTP/Veloci/GRP570-1.p.ma logic/equality.ma
3 dependent_guarded_bove_capretta.ma nat/nat.ma
4 interactive/test5.ma 
5 TPTP/Veloci/SYN083-1.p.ma logic/equality.ma
6 TPTP/Veloci/COL008-1.p.ma logic/equality.ma
7 TPTP/Veloci/GRP604-1.p.ma logic/equality.ma
8 record.ma 
9 TPTP/Veloci/COL060-3.p.ma logic/equality.ma
10 TPTP/Veloci/GRP516-1.p.ma logic/equality.ma
11 TPTP/Veloci/COL016-1.p.ma logic/equality.ma
12 TPTP/Veloci/GRP612-1.p.ma logic/equality.ma
13 reduction_old_preamble.ma 
14 TPTP/Veloci/COL024-1.p.ma logic/equality.ma
15 TPTP/Veloci/GRP139-1.p.ma logic/equality.ma
16 TPTP/Veloci/BOO006-2.p.ma logic/equality.ma
17 TPTP/Veloci/ROB010-1.p.ma logic/equality.ma
18 TPTP/Veloci/LCL157-1.p.ma logic/equality.ma
19 TPTP/Veloci/LCL132-1.p.ma logic/equality.ma
20 constructor.ma coq.ma
21 TPTP/Veloci/GRP565-1.p.ma logic/equality.ma
22 elim.ma coq.ma
23 TPTP/Veloci/GRP155-1.p.ma logic/equality.ma
24 TPTP/Veloci/BOO004-4.p.ma logic/equality.ma
25 TPTP/Veloci/LCL140-1.p.ma logic/equality.ma
26 TPTP/Veloci/GRP598-1.p.ma logic/equality.ma
27 TPTP/Veloci/GRP573-1.p.ma logic/equality.ma
28 TPTP/Veloci/GRP188-1.p.ma logic/equality.ma
29 TPTP/Veloci/GRP485-1.p.ma logic/equality.ma
30 TPTP/Veloci/GRP460-1.p.ma logic/equality.ma
31 TPTP/Veloci/GRP163-1.p.ma logic/equality.ma
32 TPTP/Veloci/BOO012-4.p.ma logic/equality.ma
33 TPTP/Veloci/GRP581-1.p.ma logic/equality.ma
34 TPTP/Veloci/GRP493-1.p.ma logic/equality.ma
35 TPTP/Veloci/COL063-3.p.ma logic/equality.ma
36 TPTP/Veloci/LCL112-2.p.ma logic/equality.ma
37 formal_topology.ma logic/connectives.ma
38 esempio_oliboni.ma logic/equality.ma nat/nat.ma
39 TPTP/Veloci/RNG023-7.p.ma logic/equality.ma
40 test2.ma coq.ma
41 replace.ma coq.ma
42 TPTP/Veloci/COL064-7.p.ma logic/equality.ma
43 TPTP/Veloci/BOO009-2.p.ma logic/equality.ma
44 TPTP/Veloci/GRP510-1.p.ma logic/equality.ma
45 TPTP/Veloci/COL010-1.p.ma logic/equality.ma
46 TPTP/Veloci/COL061-2.p.ma logic/equality.ma
47 TPTP/Veloci/BOO017-2.p.ma logic/equality.ma
48 TPTP/Veloci/LCL135-1.p.ma logic/equality.ma
49 elim_pattern.ma nat/plus.ma
50 assumption.ma coq.ma
51 interactive/grafite.ma 
52 TPTP/Veloci/GRP551-1.p.ma logic/equality.ma
53 TPTP/Veloci/GRP141-1.p.ma logic/equality.ma
54 TPTP/Veloci/GRP463-1.p.ma logic/equality.ma
55 fix_betareduction.ma coq.ma
56 TPTP/Veloci/GRP606-1.p.ma logic/equality.ma
57 coercions_dependent.ma decidable_kit/list_aux.ma list/list.ma nat/nat.ma
58 TPTP/Veloci/GRP518-1.p.ma logic/equality.ma
59 TPTP/Veloci/GRP584-1.p.ma logic/equality.ma
60 paramodulation/boolean_algebra.ma coq.ma
61 TPTP/Veloci/GRP496-1.p.ma logic/equality.ma
62 TPTP/Veloci/COL084-1.p.ma logic/equality.ma
63 TPTP/Veloci/GRP174-1.p.ma logic/equality.ma
64 TPTP/Veloci/RNG011-5.p.ma logic/equality.ma
65 TPTP/Veloci/GRP614-1.p.ma logic/equality.ma
66 inversion.ma coq.ma
67 TPTP/Veloci/GRP592-1.p.ma logic/equality.ma
68 bad_tests/baseuri.ma 
69 TPTP/Veloci/GRP182-1.p.ma logic/equality.ma
70 TPTP/Veloci/GRP116-1.p.ma logic/equality.ma
71 coercions.ma nat/compare.ma nat/times.ma
72 TPTP/Veloci/GRP011-4.p.ma logic/equality.ma
73 TPTP/Veloci/GRP149-1.p.ma logic/equality.ma
74 TPTP/Veloci/COL013-1.p.ma logic/equality.ma
75 TPTP/Veloci/GRP567-1.p.ma logic/equality.ma
76 TPTP/Veloci/COL064-2.p.ma logic/equality.ma
77 comments.ma coq.ma
78 TPTP/Veloci/COL021-1.p.ma logic/equality.ma
79 TPTP/Veloci/BOO006-4.p.ma logic/equality.ma
80 TPTP/Veloci/BOO003-2.p.ma logic/equality.ma
81 TPTP/Veloci/RNG024-6.p.ma logic/equality.ma
82 bool.ma coq.ma
83 ng_tactics.ma logic/connectives.ma nat/plus.ma ng_pts.ma
84 TPTP/Veloci/BOO011-2.p.ma logic/equality.ma
85 TPTP/Veloci/LCL154-1.p.ma logic/equality.ma
86 ng_auto.ma 
87 TPTP/Veloci/LCL114-2.p.ma logic/equality.ma
88 letrec.ma 
89 TPTP/Veloci/BOO001-1.p.ma logic/equality.ma
90 TPTP/Veloci/GRP160-1.p.ma logic/equality.ma
91 TPTP/Veloci/GRP600-1.p.ma logic/equality.ma
92 TPTP/Veloci/GRP512-1.p.ma logic/equality.ma
93 TPTP/Veloci/COL063-5.p.ma logic/equality.ma
94 continuationals.ma coq.ma
95 TPTP/Veloci/GRP490-1.p.ma logic/equality.ma
96 TPTP/Veloci/BOO034-1.p.ma logic/equality.ma
97 ng_pts.ma 
98 fold.ma coq.ma
99 TPTP/Veloci/GRP545-1.p.ma logic/equality.ma
100 TPTP/Veloci/GRP520-1.p.ma logic/equality.ma
101 TPTP/Veloci/GRP457-1.p.ma logic/equality.ma
102 TPTP/Veloci/COL064-9.p.ma logic/equality.ma
103 TPTP/Veloci/BOO009-4.p.ma logic/equality.ma
104 TPTP/Veloci/LAT040-1.p.ma logic/equality.ma
105 TPTP/Veloci/GRP578-1.p.ma logic/equality.ma
106 change.ma coq.ma
107 TPTP/Veloci/GRP143-1.p.ma logic/equality.ma
108 TPTP/Veloci/BOO075-1.p.ma logic/equality.ma
109 TPTP/Veloci/GRP168-1.p.ma logic/equality.ma
110 TPTP/Veloci/GRP586-1.p.ma logic/equality.ma
111 TPTP/Veloci/GRP561-1.p.ma logic/equality.ma
112 reduction_old.ma reduction_old_preamble.ma
113 TPTP/Veloci/GRP498-1.p.ma logic/equality.ma
114 TPTP/Veloci/GRP176-1.p.ma logic/equality.ma
115 overred.ma logic/equality.ma
116 TPTP/Veloci/COL007-1.p.ma logic/equality.ma
117 reduction_new.ma reduction_new_preamble.ma
118 TPTP/Veloci/COL058-2.p.ma logic/equality.ma
119 TPTP/Veloci/GRP603-1.p.ma logic/equality.ma
120 TPTP/Veloci/GRP515-1.p.ma logic/equality.ma
121 TPTP/Veloci/COL015-1.p.ma logic/equality.ma
122 TPTP/Veloci/RNG007-4.p.ma logic/equality.ma
123 TPTP/Veloci/GRP548-1.p.ma logic/equality.ma
124 TPTP/Veloci/GRP182-3.p.ma logic/equality.ma
125 TPTP/Veloci/COL048-1.p.ma logic/equality.ma
126 TPTP/Veloci/GRP189-2.p.ma logic/equality.ma
127 TPTP/Veloci/BOO005-2.p.ma logic/equality.ma
128 TPTP/Veloci/GRP556-1.p.ma logic/equality.ma
129 TPTP/Veloci/GRP146-1.p.ma logic/equality.ma
130 TPTP/Veloci/COL064-4.p.ma logic/equality.ma
131 TPTP/Veloci/LCL156-1.p.ma logic/equality.ma
132 contradiction.ma coq.ma
133 TPTP/Veloci/GRP564-1.p.ma logic/equality.ma
134 inversion2.ma coq.ma
135 TPTP/Veloci/GRP154-1.p.ma logic/equality.ma
136 TPTP/Veloci/BOO003-4.p.ma logic/equality.ma
137 TPTP/Veloci/ROB009-1.p.ma logic/equality.ma
138 TPTP/Veloci/LCL164-1.p.ma logic/equality.ma
139 ng_elim.ma ng_pts.ma
140 TPTP/Veloci/GRP597-1.p.ma logic/equality.ma
141 TPTP/Veloci/GRP572-1.p.ma logic/equality.ma
142 TPTP/Veloci/GRP484-1.p.ma logic/equality.ma
143 TPTP/Veloci/GRP162-1.p.ma logic/equality.ma
144 fix_che_non_passa_ma_dovrebbe.ma list/list.ma nat/nat.ma
145 subsumption.ma logic/equality.ma
146 TPTP/Veloci/BOO011-4.p.ma logic/equality.ma
147 TPTP/Veloci/GRP580-1.p.ma logic/equality.ma
148 TPTP/Veloci/COL062-3.p.ma logic/equality.ma
149 TPTP/Veloci/GRP492-1.p.ma logic/equality.ma
150 cut.ma coq.ma
151 TPTP/Veloci/LAT034-1.p.ma logic/equality.ma
152 TPTP/Veloci/COL018-1.p.ma logic/equality.ma
153 coercions_contravariant.ma logic/equality.ma nat/nat.ma
154 tinycals.ma logic/connectives.ma
155 interactive/automatic_insertion.ma 
156 clearbody.ma coq.ma
157 ng_copy2.ma ng_copy.ma
158 TPTP/Veloci/COL060-2.p.ma logic/equality.ma
159 TPTP/Veloci/LCL134-1.p.ma logic/equality.ma
160 TPTP/Veloci/BOO016-2.p.ma logic/equality.ma
161 TPTP/Veloci/LAT039-2.p.ma logic/equality.ma
162 TPTP/Veloci/GRP542-1.p.ma logic/equality.ma
163 TPTP/Veloci/GRP454-1.p.ma logic/equality.ma
164 TPTP/Veloci/GRP186-4.p.ma logic/equality.ma
165 TPTP/Veloci/GRP157-1.p.ma logic/equality.ma
166 TPTP/Veloci/GRP509-1.p.ma logic/equality.ma
167 TPTP/Veloci/GRP550-1.p.ma logic/equality.ma
168 ng_commands.ma nat/nat.ma ng_pts.ma
169 TPTP/Veloci/GRP487-1.p.ma logic/equality.ma
170 paratest.ma nat/plus.ma
171 TPTP/Veloci/GRP605-1.p.ma logic/equality.ma
172 paramodulation/BOO075-1.ma 
173 fguidi.ma logic/connectives.ma nat/nat.ma
174 TPTP/Veloci/GRP583-1.p.ma logic/equality.ma
175 TPTP/Veloci/GRP517-1.p.ma logic/equality.ma
176 TPTP/Veloci/GRP495-1.p.ma logic/equality.ma
177 TPTP/Veloci/COL083-1.p.ma logic/equality.ma
178 TPTP/Veloci/GRP173-1.p.ma logic/equality.ma
179 coercions_propagation.ma logic/connectives.ma nat/orders.ma
180 TPTP/Veloci/LAT045-1.p.ma logic/equality.ma
181 TPTP/Veloci/GRP558-1.p.ma logic/equality.ma
182 TPTP/Veloci/GRP010-4.p.ma logic/equality.ma
183 interactive/test_instance.ma 
184 TPTP/Veloci/COL012-1.p.ma logic/equality.ma
185 ng_lexiconn.ma ng_pts.ma
186 TPTP/Veloci/COL063-2.p.ma logic/equality.ma
187 first.ma 
188 ng_coercions.ma ng_pts.ma
189 TPTP/Veloci/BOO005-4.p.ma logic/equality.ma
190 TPTP/Veloci/COL045-1.p.ma logic/equality.ma
191 interactive/test7.ma 
192 bad_induction.ma logic/equality.ma nat/nat.ma
193 TPTP/Veloci/RNG023-6.p.ma logic/equality.ma
194 ng_include.ma nat/plus.ma ng_pts.ma
195 color.ma logic/equality.ma nat/nat.ma
196 TPTP/Veloci/COL064-6.p.ma logic/equality.ma
197 apply2.ma nat/nat.ma
198 metasenv_ordering.ma coq.ma
199 TPTP/Veloci/LCL153-1.p.ma logic/equality.ma
200 TPTP/Veloci/GRP608-1.p.ma logic/equality.ma
201 TPTP/Veloci/BOO010-2.p.ma logic/equality.ma
202 pullback.ma logic/equality.ma
203 TPTP/Veloci/COL086-1.p.ma logic/equality.ma
204 TPTP/Veloci/GRP151-1.p.ma logic/equality.ma
205 reduction_new_preamble.ma 
206 TPTP/Veloci/LCL161-1.p.ma logic/equality.ma
207 TPTP/Veloci/GRP616-1.p.ma logic/equality.ma
208 TPTP/Veloci/GRP206-1.p.ma logic/equality.ma
209 TPTP/Veloci/GRP023-2.p.ma logic/equality.ma
210 decompose.ma logic/connectives.ma
211 TPTP/Veloci/GRP481-1.p.ma logic/equality.ma
212 TPTP/Veloci/GRP118-1.p.ma logic/equality.ma
213 generalize.ma coq.ma
214 TPTP/Veloci/GRP511-1.p.ma logic/equality.ma
215 TPTP/Veloci/GRP192-1.p.ma logic/equality.ma
216 TPTP/Veloci/GRP569-1.p.ma logic/equality.ma
217 TPTP/Veloci/GRP544-1.p.ma logic/equality.ma
218 dependent_type_inference.ma nat/nat.ma
219 TPTP/Veloci/GRP456-1.p.ma logic/equality.ma
220 TPTP/Veloci/GRP159-1.p.ma logic/equality.ma
221 TPTP/Veloci/ROB030-1.p.ma logic/equality.ma
222 TPTP/Veloci/GRP552-1.p.ma logic/equality.ma
223 TPTP/Veloci/GRP577-1.p.ma logic/equality.ma
224 TPTP/Veloci/BOO013-2.p.ma logic/equality.ma
225 rewrite.ma coq.ma
226 TPTP/Veloci/GRP497-1.p.ma logic/equality.ma
227 bad_tests/auto.ma coq.ma
228 diabolic_fix.ma nat/nat.ma
229 TPTP/Veloci/GRP001-2.p.ma logic/equality.ma
230 test4.ma coq.ma
231 clear.ma coq.ma
232 TPTP/Veloci/GRP602-1.p.ma logic/equality.ma
233 TPTP/Veloci/GRP514-1.p.ma logic/equality.ma
234 TPTP/Veloci/LCL139-1.p.ma logic/equality.ma
235 TPTP/Veloci/GRP547-1.p.ma logic/equality.ma
236 TPTP/Veloci/BOO069-1.p.ma logic/equality.ma
237 TPTP/Veloci/GRP459-1.p.ma logic/equality.ma
238 TPTP/Veloci/GRP137-1.p.ma logic/equality.ma
239 TPTP/Veloci/COL004-3.p.ma logic/equality.ma
240 TPTP/Veloci/GRP188-2.p.ma logic/equality.ma
241 apply.ma coq.ma
242 TPTP/Veloci/GRP467-1.p.ma logic/equality.ma
243 TPTP/Veloci/GRP145-1.p.ma logic/equality.ma
244 TPTP/Veloci/LCL155-1.p.ma logic/equality.ma
245 TPTP/Veloci/COL063-4.p.ma logic/equality.ma
246 TPTP/Veloci/GRP588-1.p.ma logic/equality.ma
247 TPTP/Veloci/GRP153-1.p.ma logic/equality.ma
248 paramodulation.ma coq.ma
249 TPTP/Veloci/GRP596-1.p.ma logic/equality.ma
250 coercions_nonuniform.ma 
251 TPTP/Veloci/GRP161-1.p.ma logic/equality.ma
252 TPTP/Veloci/COL064-8.p.ma logic/equality.ma
253 TPTP/Veloci/LDA001-1.p.ma logic/equality.ma
254 TPTP/Veloci/BOO010-4.p.ma logic/equality.ma
255 TPTP/Veloci/COL050-1.p.ma logic/equality.ma
256 TPTP/Veloci/LCL110-2.p.ma logic/equality.ma
257 TPTP/Veloci/GRP491-1.p.ma logic/equality.ma
258 TPTP/Veloci/COL061-3.p.ma logic/equality.ma
259 TPTP/Veloci/COL017-1.p.ma logic/equality.ma
260 TPTP/Veloci/GRP613-1.p.ma logic/equality.ma
261 compose.ma logic/equality.ma
262 TPTP/Veloci/COL025-1.p.ma logic/equality.ma
263 TPTP/Veloci/GRP115-1.p.ma logic/equality.ma
264 unifhint.ma list/list.ma nat/nat.ma nat/plus.ma
265 letrecand.ma nat/nat.ma
266 hard_refine.ma coq.ma
267 paramodulation/group.ma coq.ma
268 TPTP/Veloci/LCL158-1.p.ma logic/equality.ma
269 TPTP/Veloci/LCL133-1.p.ma logic/equality.ma
270 TPTP/Veloci/GRP566-1.p.ma logic/equality.ma
271 TPTP/Veloci/GRP541-1.p.ma logic/equality.ma
272 decl.ma nat/orders.ma nat/times.ma
273 TPTP/Veloci/GRP156-1.p.ma logic/equality.ma
274 mysql_escaping.ma 
275 TPTP/Veloci/LCL141-1.p.ma logic/equality.ma
276 TPTP/Veloci/GRP182-2.p.ma logic/equality.ma
277 interactive/drop.ma 
278 interactive/test6.ma 
279 TPTP/Veloci/GRP599-1.p.ma logic/equality.ma
280 TPTP/Veloci/GRP574-1.p.ma logic/equality.ma
281 TPTP/Veloci/LDA007-3.p.ma logic/equality.ma
282 unfold.ma coq.ma
283 TPTP/Veloci/GRP486-1.p.ma logic/equality.ma
284 TPTP/Veloci/GRP189-1.p.ma logic/equality.ma
285 TPTP/Veloci/BOO071-1.p.ma logic/equality.ma
286 TPTP/Veloci/BOO013-4.p.ma logic/equality.ma
287 TPTP/Veloci/GRP582-1.p.ma logic/equality.ma
288 TPTP/Veloci/GRP494-1.p.ma logic/equality.ma
289 TPTP/Veloci/COL064-3.p.ma logic/equality.ma
290 TPTP/Veloci/LCL113-2.p.ma logic/equality.ma
291 TPTP/Veloci/RNG008-4.p.ma logic/equality.ma
292 demodulation_matita.ma nat/minus.ma
293 TPTP/Veloci/ROB002-1.p.ma logic/equality.ma
294 tacticals.ma 
295 TPTP/Veloci/GRP549-1.p.ma logic/equality.ma
296 TPTP/Veloci/GRP001-4.p.ma logic/equality.ma
297 TPTP/Veloci/GRP590-1.p.ma logic/equality.ma
298 applys.ma nat/div_and_mod.ma nat/factorial.ma nat/primes.ma
299 TPTP/Veloci/RNG024-7.p.ma logic/equality.ma
300 injection.ma coq.ma
301 second.ma first.ma
302 TPTP/Veloci/COL062-2.p.ma logic/equality.ma
303 match_inference.ma 
304 ng_includeB.ma ng_include.ma
305 unifhint_simple.ma logic/equality.ma
306 simpl.ma coq.ma
307 TPTP/Veloci/COL063-6.p.ma logic/equality.ma
308 TPTP/Veloci/GRP142-1.p.ma logic/equality.ma
309 third.ma first.ma second.ma
310 TPTP/Veloci/GRP560-1.p.ma logic/equality.ma
311 ng_coercion_and_hints.ma ng_pts.ma
312 TPTP/Veloci/GRP150-1.p.ma logic/equality.ma
313 TPTP/Veloci/COL085-1.p.ma logic/equality.ma
314 TPTP/Veloci/GRP615-1.p.ma logic/equality.ma
315 TPTP/Veloci/LAT039-1.p.ma logic/equality.ma
316 luo.ma Z/times.ma logic/equality.ma
317 TPTP/Veloci/GRP022-2.p.ma logic/equality.ma
318 TPTP/Veloci/GRP186-3.p.ma logic/equality.ma
319 coercions_russell.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma list/sort.ma nat/compare.ma nat/orders.ma
320 ng_copy.ma 
321 TPTP/Veloci/GRP117-1.p.ma logic/equality.ma
322 multiple_inheritance.ma logic/equality.ma
323 test3.ma coq.ma
324 TPTP/Veloci/ROB013-1.p.ma logic/equality.ma
325 TPTP/Veloci/GRP168-2.p.ma logic/equality.ma
326 TPTP/Veloci/GRP012-4.p.ma logic/equality.ma
327 naiveparamod.ma logic/equality.ma
328 TPTP/Veloci/GRP176-2.p.ma logic/equality.ma
329 TPTP/Veloci/COL014-1.p.ma logic/equality.ma
330 TPTP/Veloci/GRP568-1.p.ma logic/equality.ma
331 TPTP/Veloci/GRP543-1.p.ma logic/equality.ma
332 TPTP/Veloci/GRP455-1.p.ma logic/equality.ma
333 TPTP/Veloci/GRP158-1.p.ma logic/equality.ma
334 TPTP/Veloci/COL022-1.p.ma logic/equality.ma
335 TPTP/Veloci/BOO004-2.p.ma logic/equality.ma
336 TPTP/Veloci/GRP576-1.p.ma logic/equality.ma
337 TPTP/Veloci/GRP488-1.p.ma logic/equality.ma
338 TPTP/Veloci/COL058-3.p.ma logic/equality.ma
339 dependent_injection.ma coq.ma
340 TPTP/Veloci/BOO012-2.p.ma logic/equality.ma
341 TPTP/Veloci/LCL115-2.p.ma logic/equality.ma
342 absurd.ma coq.ma
343 TPTP/Veloci/GRP182-4.p.ma logic/equality.ma
344 destruct.ma datatypes/constructors.ma logic/equality.ma nat/nat.ma
345 TPTP/Veloci/COL064-5.p.ma logic/equality.ma
346 TPTP/Veloci/GRP513-1.p.ma logic/equality.ma
347 TPTP/Veloci/LAT033-1.p.ma logic/equality.ma
348 TPTP/Veloci/GRP546-1.p.ma logic/equality.ma
349 TPTP/Veloci/GRP136-1.p.ma logic/equality.ma
350 TPTP/Veloci/GRP458-1.p.ma logic/equality.ma
351 coercions_open.ma logic/equality.ma nat/nat.ma
352 paramodulation/irratsqrt2.ma nat/minus.ma nat/times.ma
353 ng_uris_and_notation.ma nat/nat.ma ng_pts.ma
354 TPTP/Veloci/GRP144-1.p.ma logic/equality.ma
355 TPTP/Veloci/LAT008-1.p.ma logic/equality.ma
356 TPTP/Veloci/BOO018-4.p.ma logic/equality.ma
357 demodulation_coq.ma coq.ma
358 TPTP/Veloci/GRP562-1.p.ma logic/equality.ma
359 TPTP/Veloci/GRP152-1.p.ma logic/equality.ma
360 Z/times.ma 
361 coq.ma 
362 datatypes/bool.ma 
363 datatypes/constructors.ma 
364 decidable_kit/list_aux.ma 
365 list/list.ma 
366 list/sort.ma 
367 logic/connectives.ma 
368 logic/equality.ma 
369 nat/compare.ma 
370 nat/div_and_mod.ma 
371 nat/factorial.ma 
372 nat/minus.ma 
373 nat/nat.ma 
374 nat/orders.ma 
375 nat/plus.ma 
376 nat/primes.ma 
377 nat/times.ma