1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 universe constraint Type[0] < Type[1].
24 universe constraint Type[1] < Type[2].
25 universe constraint Type[2] < Type[3].
27 (* ********************************** *)
28 (* SOTTOINSIEME MINIMALE DELLA TEORIA *)
29 (* ********************************** *)
31 (* logic/connectives.ma *)
33 ninductive True: Prop ≝
36 ninductive False: Prop ≝.
38 ndefinition Not: Prop → Prop ≝
41 interpretation "logical not" 'not x = (Not x).
44 nlemma absurd : ∀A,C:Prop.A → ¬A → C.
51 nlemma not_to_not : ∀A,B:Prop. (A → B) → ((¬B) → (¬A)).
58 nlemma prop_to_nnprop : ∀P.P → ¬¬P.
59 #P; nnormalize; #H; #H1;
63 ninductive And2 (A,B:Prop) : Prop ≝
64 conj2 : A → B → (And2 A B).
66 interpretation "logical and" 'and x y = (And2 x y).
68 nlemma proj2_1: ∀A,B:Prop.A ∧ B → A.
70 napply (And2_ind A B … H);
75 nlemma proj2_2: ∀A,B:Prop.A ∧ B → B.
77 napply (And2_ind A B … H);
82 ninductive And3 (A,B,C:Prop) : Prop ≝
83 conj3 : A → B → C → (And3 A B C).
85 nlemma proj3_1: ∀A,B,C:Prop.And3 A B C → A.
87 napply (And3_ind A B C … H);
92 nlemma proj3_2: ∀A,B,C:Prop.And3 A B C → B.
94 napply (And3_ind A B C … H);
99 nlemma proj3_3: ∀A,B,C:Prop.And3 A B C → C.
101 napply (And3_ind A B C … H);
106 ninductive And4 (A,B,C,D:Prop) : Prop ≝
107 conj4 : A → B → C → D → (And4 A B C D).
109 nlemma proj4_1: ∀A,B,C,D:Prop.And4 A B C D → A.
111 napply (And4_ind A B C D … H);
116 nlemma proj4_2: ∀A,B,C,D:Prop.And4 A B C D → B.
118 napply (And4_ind A B C D … H);
123 nlemma proj4_3: ∀A,B,C,D:Prop.And4 A B C D → C.
125 napply (And4_ind A B C D … H);
130 nlemma proj4_4: ∀A,B,C,D:Prop.And4 A B C D → D.
132 napply (And4_ind A B C D … H);
137 ninductive And5 (A,B,C,D,E:Prop) : Prop ≝
138 conj5 : A → B → C → D → E → (And5 A B C D E).
140 nlemma proj5_1: ∀A,B,C,D,E:Prop.And5 A B C D E → A.
141 #A; #B; #C; #D; #E; #H;
142 napply (And5_ind A B C D E … H);
143 #H1; #H2; #H3; #H4; #H5;
147 nlemma proj5_2: ∀A,B,C,D,E:Prop.And5 A B C D E → B.
148 #A; #B; #C; #D; #E; #H;
149 napply (And5_ind A B C D E … H);
150 #H1; #H2; #H3; #H4; #H5;
154 nlemma proj5_3: ∀A,B,C,D,E:Prop.And5 A B C D E → C.
155 #A; #B; #C; #D; #E; #H;
156 napply (And5_ind A B C D E … H);
157 #H1; #H2; #H3; #H4; #H5;
161 nlemma proj5_4: ∀A,B,C,D,E:Prop.And5 A B C D E → D.
162 #A; #B; #C; #D; #E; #H;
163 napply (And5_ind A B C D E … H);
164 #H1; #H2; #H3; #H4; #H5;
168 nlemma proj5_5: ∀A,B,C,D,E:Prop.And5 A B C D E → E.
169 #A; #B; #C; #D; #E; #H;
170 napply (And5_ind A B C D E … H);
171 #H1; #H2; #H3; #H4; #H5;
175 ninductive Or2 (A,B:Prop) : Prop ≝
176 or2_intro1 : A → (Or2 A B)
177 | or2_intro2 : B → (Or2 A B).
179 interpretation "logical or" 'or x y = (Or2 x y).
182 : ∀P1,P2,Q:Prop.Or2 P1 P2 → ∀f1:P1 → Q.∀f2:P2 → Q.Q.
183 #P1; #P2; #Q; #H; #f1; #f2;
184 napply (Or2_ind P1 P2 ? f1 f2 ?);
188 nlemma symmetric_or2 : ∀P1,P2.Or2 P1 P2 → Or2 P2 P1.
190 napply (or2_elim P1 P2 ? H);
191 ##[ ##1: #H1; napply (or2_intro2 P2 P1 H1)
192 ##| ##2: #H1; napply (or2_intro1 P2 P1 H1)
196 ninductive Or3 (A,B,C:Prop) : Prop ≝
197 or3_intro1 : A → (Or3 A B C)
198 | or3_intro2 : B → (Or3 A B C)
199 | or3_intro3 : C → (Or3 A B C).
202 : ∀P1,P2,P3,Q:Prop.Or3 P1 P2 P3 → ∀f1:P1 → Q.∀f2:P2 → Q.∀f3:P3 → Q.Q.
203 #P1; #P2; #P3; #Q; #H; #f1; #f2; #f3;
204 napply (Or3_ind P1 P2 P3 ? f1 f2 f3 ?);
208 nlemma symmetric_or3_12 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P2 P1 P3.
210 napply (or3_elim P1 P2 P3 ? H);
211 ##[ ##1: #H1; napply (or3_intro2 P2 P1 P3 H1)
212 ##| ##2: #H1; napply (or3_intro1 P2 P1 P3 H1)
213 ##| ##3: #H1; napply (or3_intro3 P2 P1 P3 H1)
217 nlemma symmetric_or3_13 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P3 P2 P1.
219 napply (or3_elim P1 P2 P3 ? H);
220 ##[ ##1: #H1; napply (or3_intro3 P3 P2 P1 H1)
221 ##| ##2: #H1; napply (or3_intro2 P3 P2 P1 H1)
222 ##| ##3: #H1; napply (or3_intro1 P3 P2 P1 H1)
226 nlemma symmetric_or3_23 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P1 P3 P2.
228 napply (or3_elim P1 P2 P3 ? H);
229 ##[ ##1: #H1; napply (or3_intro1 P1 P3 P2 H1)
230 ##| ##2: #H1; napply (or3_intro3 P1 P3 P2 H1)
231 ##| ##3: #H1; napply (or3_intro2 P1 P3 P2 H1)
235 ninductive Or4 (A,B,C,D:Prop) : Prop ≝
236 or4_intro1 : A → (Or4 A B C D)
237 | or4_intro2 : B → (Or4 A B C D)
238 | or4_intro3 : C → (Or4 A B C D)
239 | or4_intro4 : D → (Or4 A B C D).
242 : ∀P1,P2,P3,P4,Q:Prop.Or4 P1 P2 P3 P4 → ∀f1:P1 → Q.∀f2:P2 → Q.
243 ∀f3:P3 → Q.∀f4:P4 → Q.Q.
244 #P1; #P2; #P3; #P4; #Q; #H; #f1; #f2; #f3; #f4;
245 napply (Or4_ind P1 P2 P3 P4 ? f1 f2 f3 f4 ?);
249 nlemma symmetric_or4_12 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P2 P1 P3 P4.
250 #P1; #P2; #P3; #P4; #H;
251 napply (or4_elim P1 P2 P3 P4 ? H);
252 ##[ ##1: #H1; napply (or4_intro2 P2 P1 P3 P4 H1)
253 ##| ##2: #H1; napply (or4_intro1 P2 P1 P3 P4 H1)
254 ##| ##3: #H1; napply (or4_intro3 P2 P1 P3 P4 H1)
255 ##| ##4: #H1; napply (or4_intro4 P2 P1 P3 P4 H1)
259 nlemma symmetric_or4_13 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P3 P2 P1 P4.
260 #P1; #P2; #P3; #P4; #H;
261 napply (or4_elim P1 P2 P3 P4 ? H);
262 ##[ ##1: #H1; napply (or4_intro3 P3 P2 P1 P4 H1)
263 ##| ##2: #H1; napply (or4_intro2 P3 P2 P1 P4 H1)
264 ##| ##3: #H1; napply (or4_intro1 P3 P2 P1 P4 H1)
265 ##| ##4: #H1; napply (or4_intro4 P3 P2 P1 P4 H1)
269 nlemma symmetric_or4_14 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P4 P2 P3 P1.
270 #P1; #P2; #P3; #P4; #H;
271 napply (or4_elim P1 P2 P3 P4 ? H);
272 ##[ ##1: #H1; napply (or4_intro4 P4 P2 P3 P1 H1)
273 ##| ##2: #H1; napply (or4_intro2 P4 P2 P3 P1 H1)
274 ##| ##3: #H1; napply (or4_intro3 P4 P2 P3 P1 H1)
275 ##| ##4: #H1; napply (or4_intro1 P4 P2 P3 P1 H1)
279 nlemma symmetric_or4_23 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P3 P2 P4.
280 #P1; #P2; #P3; #P4; #H;
281 napply (or4_elim P1 P2 P3 P4 ? H);
282 ##[ ##1: #H1; napply (or4_intro1 P1 P3 P2 P4 H1)
283 ##| ##2: #H1; napply (or4_intro3 P1 P3 P2 P4 H1)
284 ##| ##3: #H1; napply (or4_intro2 P1 P3 P2 P4 H1)
285 ##| ##4: #H1; napply (or4_intro4 P1 P3 P2 P4 H1)
289 nlemma symmetric_or4_24 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P4 P3 P2.
290 #P1; #P2; #P3; #P4; #H;
291 napply (or4_elim P1 P2 P3 P4 ? H);
292 ##[ ##1: #H1; napply (or4_intro1 P1 P4 P3 P2 H1)
293 ##| ##2: #H1; napply (or4_intro4 P1 P4 P3 P2 H1)
294 ##| ##3: #H1; napply (or4_intro3 P1 P4 P3 P2 H1)
295 ##| ##4: #H1; napply (or4_intro2 P1 P4 P3 P2 H1)
299 nlemma symmetric_or4_34 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P2 P4 P3.
300 #P1; #P2; #P3; #P4; #H;
301 napply (or4_elim P1 P2 P3 P4 ? H);
302 ##[ ##1: #H1; napply (or4_intro1 P1 P2 P4 P3 H1)
303 ##| ##2: #H1; napply (or4_intro2 P1 P2 P4 P3 H1)
304 ##| ##3: #H1; napply (or4_intro4 P1 P2 P4 P3 H1)
305 ##| ##4: #H1; napply (or4_intro3 P1 P2 P4 P3 H1)
309 ninductive Or5 (A,B,C,D,E:Prop) : Prop ≝
310 or5_intro1 : A → (Or5 A B C D E)
311 | or5_intro2 : B → (Or5 A B C D E)
312 | or5_intro3 : C → (Or5 A B C D E)
313 | or5_intro4 : D → (Or5 A B C D E)
314 | or5_intro5 : E → (Or5 A B C D E).
317 : ∀P1,P2,P3,P4,P5,Q:Prop.Or5 P1 P2 P3 P4 P5 → ∀f1:P1 → Q.∀f2:P2 → Q.
318 ∀f3:P3 → Q.∀f4:P4 → Q.∀f5:P5 → Q.Q.
319 #P1; #P2; #P3; #P4; #P5; #Q; #H; #f1; #f2; #f3; #f4; #f5;
320 napply (Or5_ind P1 P2 P3 P4 P5 ? f1 f2 f3 f4 f5 ?);
324 nlemma symmetric_or5_12 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P2 P1 P3 P4 P5.
325 #P1; #P2; #P3; #P4; #P5; #H;
326 napply (or5_elim P1 P2 P3 P4 P5 ? H);
327 ##[ ##1: #H1; napply (or5_intro2 P2 P1 P3 P4 P5 H1)
328 ##| ##2: #H1; napply (or5_intro1 P2 P1 P3 P4 P5 H1)
329 ##| ##3: #H1; napply (or5_intro3 P2 P1 P3 P4 P5 H1)
330 ##| ##4: #H1; napply (or5_intro4 P2 P1 P3 P4 P5 H1)
331 ##| ##5: #H1; napply (or5_intro5 P2 P1 P3 P4 P5 H1)
335 nlemma symmetric_or5_13 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P3 P2 P1 P4 P5.
336 #P1; #P2; #P3; #P4; #P5; #H;
337 napply (or5_elim P1 P2 P3 P4 P5 ? H);
338 ##[ ##1: #H1; napply (or5_intro3 P3 P2 P1 P4 P5 H1)
339 ##| ##2: #H1; napply (or5_intro2 P3 P2 P1 P4 P5 H1)
340 ##| ##3: #H1; napply (or5_intro1 P3 P2 P1 P4 P5 H1)
341 ##| ##4: #H1; napply (or5_intro4 P3 P2 P1 P4 P5 H1)
342 ##| ##5: #H1; napply (or5_intro5 P3 P2 P1 P4 P5 H1)
346 nlemma symmetric_or5_14 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P4 P2 P3 P1 P5.
347 #P1; #P2; #P3; #P4; #P5; #H;
348 napply (or5_elim P1 P2 P3 P4 P5 ? H);
349 ##[ ##1: #H1; napply (or5_intro4 P4 P2 P3 P1 P5 H1)
350 ##| ##2: #H1; napply (or5_intro2 P4 P2 P3 P1 P5 H1)
351 ##| ##3: #H1; napply (or5_intro3 P4 P2 P3 P1 P5 H1)
352 ##| ##4: #H1; napply (or5_intro1 P4 P2 P3 P1 P5 H1)
353 ##| ##5: #H1; napply (or5_intro5 P4 P2 P3 P1 P5 H1)
357 nlemma symmetric_or5_15 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P5 P2 P3 P4 P1.
358 #P1; #P2; #P3; #P4; #P5; #H;
359 napply (or5_elim P1 P2 P3 P4 P5 ? H);
360 ##[ ##1: #H1; napply (or5_intro5 P5 P2 P3 P4 P1 H1)
361 ##| ##2: #H1; napply (or5_intro2 P5 P2 P3 P4 P1 H1)
362 ##| ##3: #H1; napply (or5_intro3 P5 P2 P3 P4 P1 H1)
363 ##| ##4: #H1; napply (or5_intro4 P5 P2 P3 P4 P1 H1)
364 ##| ##5: #H1; napply (or5_intro1 P5 P2 P3 P4 P1 H1)
368 nlemma symmetric_or5_23 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P3 P2 P4 P5.
369 #P1; #P2; #P3; #P4; #P5; #H;
370 napply (or5_elim P1 P2 P3 P4 P5 ? H);
371 ##[ ##1: #H1; napply (or5_intro1 P1 P3 P2 P4 P5 H1)
372 ##| ##2: #H1; napply (or5_intro3 P1 P3 P2 P4 P5 H1)
373 ##| ##3: #H1; napply (or5_intro2 P1 P3 P2 P4 P5 H1)
374 ##| ##4: #H1; napply (or5_intro4 P1 P3 P2 P4 P5 H1)
375 ##| ##5: #H1; napply (or5_intro5 P1 P3 P2 P4 P5 H1)
379 nlemma symmetric_or5_24 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P4 P3 P2 P5.
380 #P1; #P2; #P3; #P4; #P5; #H;
381 napply (or5_elim P1 P2 P3 P4 P5 ? H);
382 ##[ ##1: #H1; napply (or5_intro1 P1 P4 P3 P2 P5 H1)
383 ##| ##2: #H1; napply (or5_intro4 P1 P4 P3 P2 P5 H1)
384 ##| ##3: #H1; napply (or5_intro3 P1 P4 P3 P2 P5 H1)
385 ##| ##4: #H1; napply (or5_intro2 P1 P4 P3 P2 P5 H1)
386 ##| ##5: #H1; napply (or5_intro5 P1 P4 P3 P2 P5 H1)
390 nlemma symmetric_or5_25 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P5 P3 P4 P2.
391 #P1; #P2; #P3; #P4; #P5; #H;
392 napply (or5_elim P1 P2 P3 P4 P5 ? H);
393 ##[ ##1: #H1; napply (or5_intro1 P1 P5 P3 P4 P2 H1)
394 ##| ##2: #H1; napply (or5_intro5 P1 P5 P3 P4 P2 H1)
395 ##| ##3: #H1; napply (or5_intro3 P1 P5 P3 P4 P2 H1)
396 ##| ##4: #H1; napply (or5_intro4 P1 P5 P3 P4 P2 H1)
397 ##| ##5: #H1; napply (or5_intro2 P1 P5 P3 P4 P2 H1)
401 nlemma symmetric_or5_34 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P4 P3 P5.
402 #P1; #P2; #P3; #P4; #P5; #H;
403 napply (or5_elim P1 P2 P3 P4 P5 ? H);
404 ##[ ##1: #H1; napply (or5_intro1 P1 P2 P4 P3 P5 H1)
405 ##| ##2: #H1; napply (or5_intro2 P1 P2 P4 P3 P5 H1)
406 ##| ##3: #H1; napply (or5_intro4 P1 P2 P4 P3 P5 H1)
407 ##| ##4: #H1; napply (or5_intro3 P1 P2 P4 P3 P5 H1)
408 ##| ##5: #H1; napply (or5_intro5 P1 P2 P4 P3 P5 H1)
412 nlemma symmetric_or5_35 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P5 P4 P3.
413 #P1; #P2; #P3; #P4; #P5; #H;
414 napply (or5_elim P1 P2 P3 P4 P5 ? H);
415 ##[ ##1: #H1; napply (or5_intro1 P1 P2 P5 P4 P3 H1)
416 ##| ##2: #H1; napply (or5_intro2 P1 P2 P5 P4 P3 H1)
417 ##| ##3: #H1; napply (or5_intro5 P1 P2 P5 P4 P3 H1)
418 ##| ##4: #H1; napply (or5_intro4 P1 P2 P5 P4 P3 H1)
419 ##| ##5: #H1; napply (or5_intro3 P1 P2 P5 P4 P3 H1)
423 nlemma symmetric_or5_45 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P3 P5 P4.
424 #P1; #P2; #P3; #P4; #P5; #H;
425 napply (or5_elim P1 P2 P3 P4 P5 ? H);
426 ##[ ##1: #H1; napply (or5_intro1 P1 P2 P3 P5 P4 H1)
427 ##| ##2: #H1; napply (or5_intro2 P1 P2 P3 P5 P4 H1)
428 ##| ##3: #H1; napply (or5_intro3 P1 P2 P3 P5 P4 H1)
429 ##| ##4: #H1; napply (or5_intro5 P1 P2 P3 P5 P4 H1)
430 ##| ##5: #H1; napply (or5_intro4 P1 P2 P3 P5 P4 H1)
434 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
435 ex_intro: ∀x:A.Q x → ex A Q.
437 interpretation "exists" 'exists x = (ex ? x).
439 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
440 ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
443 (* higher_order_defs/relations *)
445 ndefinition relation : Type → Type ≝
446 λA:Type.A → A → Prop.
449 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
453 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
454 λA.λR.∀x,y:A.R x y → R y x.
457 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
458 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
460 ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝
461 λA.λR.∀x:A.¬ (R x x).
463 ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝
464 λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
466 ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
467 λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)).
469 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
470 λA.λR.∀x,y:A.R x y → ¬ (R y x).
473 (* logic/equality.ma *)
475 ninductive eq (A:Type) (x:A) : A → Prop ≝
478 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
480 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
483 nlemma eq_f : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.x = y → (f x) = (f y).
484 #T1; #T2; #x; #y; #f; #H;
489 nlemma eq_f2 : ∀T1,T2,T3:Type.∀x1,y1:T1.∀x2,y2:T2.∀f:T1 → T2 → T3.x1 = y1 → x2 = y2 → f x1 x2 = f y1 y2.
490 #T1; #T2; #T3; #x1; #y1; #x2; #y2; #f; #H1; #H2;
496 nlemma neqf_to_neq : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.((f x) ≠ (f y)) → x ≠ y.
497 #T1; #T2; #x; #y; #f;
499 napply (H (eq_f … H1)).
503 nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
511 nlemma eq_ind_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
512 #A; #x; #P; #H; #y; #H1;
513 nrewrite < (symmetric_eq … H1);
518 nlemma symmetric_neq : ∀T:Type.∀x,y:T.x ≠ y → y ≠ x.
522 nrewrite > H1 in H:(%); #H;
523 napply (H (refl_eq …)).
526 ndefinition relationT : Type → Type → Type ≝
529 ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
530 λA,T.λR.∀x,y:A.R x y = R y x.
532 ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
533 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).
536 ninductive bool : Type ≝
540 nlemma pippo : (true = false) → (false = true).