From 7fa016a4bb3d62c4680c02089e21ae0a307af7d0 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Fri, 7 Oct 2011 12:20:08 +0000 Subject: [PATCH] commit by user utente2 --- weblib/basics/logic.ma | 135 +++++++++++++++++++++-------------------- 1 file changed, 68 insertions(+), 67 deletions(-) diff --git a/weblib/basics/logic.ma b/weblib/basics/logic.ma index 3f92d6aad..5e97f9b5c 100644 --- a/weblib/basics/logic.ma +++ b/weblib/basics/logic.ma @@ -20,42 +20,42 @@ inductive eq (A:Type[1]) (x:A) : A → Prop ≝ interpretation "leibnitz's equality" 'eq t x y = (eq t x y). lemma eq_rect_r: - ∀A.∀a,x.∀p:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A ? x a.∀P: - ∀x:A. x A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A a → Type[2]. P a (refl A a) → P x p. + ∀A.∀a,x.∀p:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a.∀P: + ∀x:A. x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a → Type[2]. P a (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a A a) → P x p. #A #a #x #p (cases p) // qed. lemma eq_ind_r : - ∀A.∀a.∀P: ∀x:A. x A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A a → Prop. P a (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A A a) → - ∀x.∀p:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A ? x a.P x p. - #A #a #P #p #x0 #p0; @(A href="cic:/matita/basics/logic/eq_rect_r.def(1)"eq_rect_r/A ? ? ? p0) //; qed. + ∀A.∀a.∀P: ∀x:A. x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a → Prop. P a (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a A a) → + ∀x.∀p:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a.P x p. + #A #a #P #p #x0 #p0; @(a href="cic:/matita/basics/logic/eq_rect_r.def(1)"eq_rect_r/a ? ? ? p0) //; qed. lemma eq_rect_Type2_r: - ∀A.∀a.∀P: ∀x:A. A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A ? x a → Type[2]. P a (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A A a) → - ∀x.∀p:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A ? x a.P x p. + ∀A.∀a.∀P: ∀x:A. a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a → Type[2]. P a (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a A a) → + ∀x.∀p:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a.P x p. #A #a #P #H #x #p (generalize in match H) (generalize in match P) cases p; //; qed. -theorem rewrite_l: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. x A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A y → P y. +theorem rewrite_l: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y → P y. #A #x #P #Hx #y #Heq (cases Heq); //; qed. -theorem sym_eq: ∀A.∀x,y:A. x A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A y → y A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A x. -#A #x #y #Heq @(A href="cic:/matita/basics/logic/rewrite_l.def(1)"rewrite_l/A A x (λz.zA title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ax)); //; qed. +theorem sym_eq: ∀A.∀x,y:A. x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y → y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x. +#A #x #y #Heq @(a href="cic:/matita/basics/logic/rewrite_l.def(1)"rewrite_l/a A x (λz.za title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax)); //; qed. -theorem rewrite_r: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. y A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A x → P y. -#A #x #P #Hx #y #Heq (cases (A href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/A ? ? ? Heq)); //; qed. +theorem rewrite_r: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x → P y. +#A #x #P #Hx #y #Heq (cases (a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a ? ? ? Heq)); //; qed. -theorem eq_coerc: ∀A,B:Type[0].A→(AA title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/AB)→B. +theorem eq_coerc: ∀A,B:Type[0].A→(Aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aB)→B. #A #B #Ha #Heq (elim Heq); //; qed. -theorem trans_eq : ∀A.∀x,y,z:A. x A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A y → y A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A z → x A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A z. +theorem trans_eq : ∀A.∀x,y,z:A. x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y → y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a z → x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a z. #A #x #y #z #H1 #H2 >H1; //; qed. -theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. xA title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ay → f x A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A f y. +theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. xa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ay → f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f y. #A #B #f #x #y #H >H; //; qed. (* deleterio per auto? *) theorem eq_f2: ∀A,B,C.∀f:A→B→C. -∀x1,x2:A.∀y1,y2:B. x1A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ax2 → y1A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ay2 → f x1 y1 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A f x2 y2. +∀x1,x2:A.∀y1,y2:B. x1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax2 → y1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ay2 → f x1 y1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f x2 y2. #A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed. (* hint to genereric equality @@ -80,12 +80,12 @@ inductive False: Prop ≝ . λA. A → False. *) inductive Not (A:Prop): Prop ≝ -nmk: (A → A href="cic:/matita/basics/logic/False.ind(1,0,0)"False/A) → Not A. +nmk: (A → a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a) → Not A. interpretation "logical not" 'not x = (Not x). -theorem absurd : ∀A:Prop. A → A title="logical not" href="cic:/fakeuri.def(1)"¬/AA → A href="cic:/matita/basics/logic/False.ind(1,0,0)"False/A. +theorem absurd : ∀A:Prop. A → a title="logical not" href="cic:/fakeuri.def(1)"¬/aA → a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a. #A #H #Hn (elim Hn); /2/; qed. (* @@ -93,13 +93,13 @@ ntheorem absurd : ∀ A,C:Prop. A → ¬A → C. #A; #C; #H; #Hn; nelim (Hn H). nqed. *) -theorem not_to_not : ∀A,B:Prop. (A → B) → A title="logical not" href="cic:/fakeuri.def(1)"¬/AB →A title="logical not" href="cic:/fakeuri.def(1)"¬/AA. +theorem not_to_not : ∀A,B:Prop. (A → B) → a title="logical not" href="cic:/fakeuri.def(1)"¬/aB →a title="logical not" href="cic:/fakeuri.def(1)"¬/aA. /4/; qed. (* inequality *) interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)). -theorem sym_not_eq: ∀A.∀x,y:A. x A title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/A y → y A title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/A x. +theorem sym_not_eq: ∀A.∀x,y:A. x a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a y → y a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a x. /3/; qed. (* and *) @@ -108,10 +108,10 @@ inductive And (A,B:Prop) : Prop ≝ interpretation "logical and" 'and x y = (And x y). -theorem proj1: ∀A,B:Prop. A A title="logical and" href="cic:/fakeuri.def(1)"∧/A B → A. +theorem proj1: ∀A,B:Prop. A a title="logical and" href="cic:/fakeuri.def(1)"∧/a B → A. #A #B #AB (elim AB) //; qed. -theorem proj2: ∀ A,B:Prop. A A title="logical and" href="cic:/fakeuri.def(1)"∧/A B → B. +theorem proj2: ∀ A,B:Prop. A a title="logical and" href="cic:/fakeuri.def(1)"∧/a B → B. #A #B #AB (elim AB) //; qed. (* or *) @@ -122,7 +122,7 @@ inductive Or (A,B:Prop) : Prop ≝ interpretation "logical or" 'or x y = (Or x y). definition decidable : Prop → Prop ≝ -λ A:Prop. A A title="logical or" href="cic:/fakeuri.def(1)"∨/A A title="logical not" href="cic:/fakeuri.def(1)"¬/A A. +λ A:Prop. A a title="logical or" href="cic:/fakeuri.def(1)"∨/a a title="logical not" href="cic:/fakeuri.def(1)"¬/a A. (* exists *) inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝ @@ -135,7 +135,7 @@ inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝ (* iff *) definition iff := - λ A,B. (A → B) A title="logical and" href="cic:/fakeuri.def(1)"∧/A (B → A). + λ A,B. (A → B) a title="logical and" href="cic:/fakeuri.def(1)"∧/a (B → A). interpretation "iff" 'iff a b = (iff a b). @@ -143,84 +143,85 @@ interpretation "iff" 'iff a b = (iff a b). definition R0 ≝ λT:Type[0].λt:T.t. -definition R1 ≝ A href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/A. +definition R1 ≝ a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/a. (* useless stuff *) definition R2 : ∀T0:Type[0]. ∀a0:T0. - ∀T1:∀x0:T0. a0A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ax0 → Type[0]. - ∀a1:T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? a0). - ∀T2:∀x0:T0. ∀p0:a0A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ax0. ∀x1:T1 x0 p0. A href="cic:/matita/basics/logic/R1.def(2)"R1/A ?? T1 a1 ? p0 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A x1 → Type[0]. - ∀a2:T2 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? a1). + ∀T1:∀x0:T0. a0a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax0 → Type[0]. + ∀a1:T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a0). + ∀T2:∀x0:T0. ∀p0:a0a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax0. ∀x1:T1 x0 p0. a href="cic:/matita/basics/logic/R1.def(2)"R1/a ?? T1 a1 ? p0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x1 → Type[0]. + ∀a2:T2 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a1). ∀b0:T0. - ∀e0:a0 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A b0. + ∀e0:a0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b0. ∀b1: T1 b0 e0. - ∀e1:A href="cic:/matita/basics/logic/R1.def(2)"R1/A ?? T1 a1 ? e0 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A b1. + ∀e1:a href="cic:/matita/basics/logic/R1.def(2)"R1/a ?? T1 a1 ? e0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b1. T2 b0 e0 b1 e1. #T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1 -@(A href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/A ????? e1) -@(A href="cic:/matita/basics/logic/R1.def(2)"R1/A ?? ? ?? e0) +@(a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/a ????? e1) +@(a href="cic:/matita/basics/logic/R1.def(2)"R1/a ?? ? ?? e0) @a2 qed. definition R3 : ∀T0:Type[0]. ∀a0:T0. - ∀T1:∀x0:T0. a0A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ax0 → Type[0]. - ∀a1:T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? a0). - ∀T2:∀x0:T0. ∀p0:a0A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ax0. ∀x1:T1 x0 p0. A href="cic:/matita/basics/logic/R1.def(2)"R1/A ?? T1 a1 ? p0 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A x1 → Type[0]. - ∀a2:T2 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? a1). - ∀T3:∀x0:T0. ∀p0:a0A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ax0. ∀x1:T1 x0 p0.∀p1:A href="cic:/matita/basics/logic/R1.def(2)"R1/A ?? T1 a1 ? p0 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A x1. - ∀x2:T2 x0 p0 x1 p1.A href="cic:/matita/basics/logic/R2.def(3)"R2/A ???? T2 a2 x0 p0 ? p1 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A x2 → Type[0]. - ∀a3:T3 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? a1) a2 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? a2). + ∀T1:∀x0:T0. a0a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax0 → Type[0]. + ∀a1:T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a0). + ∀T2:∀x0:T0. ∀p0:a0a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax0. ∀x1:T1 x0 p0. a href="cic:/matita/basics/logic/R1.def(2)"R1/a ?? T1 a1 ? p0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x1 → Type[0]. + ∀a2:T2 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a1). + ∀T3:∀x0:T0. ∀p0:a0a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax0. ∀x1:T1 x0 p0.∀p1:a href="cic:/matita/basics/logic/R1.def(2)"R1/a ?? T1 a1 ? p0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x1. + ∀x2:T2 x0 p0 x1 p1.a href="cic:/matita/basics/logic/R2.def(3)"R2/a ???? T2 a2 x0 p0 ? p1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x2 → Type[0]. + ∀a3:T3 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a1) a2 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a2). ∀b0:T0. - ∀e0:a0 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A b0. + ∀e0:a0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b0. ∀b1: T1 b0 e0. - ∀e1:A href="cic:/matita/basics/logic/R1.def(2)"R1/A ?? T1 a1 ? e0 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A b1. + ∀e1:a href="cic:/matita/basics/logic/R1.def(2)"R1/a ?? T1 a1 ? e0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b1. ∀b2: T2 b0 e0 b1 e1. - ∀e2:A href="cic:/matita/basics/logic/R2.def(3)"R2/A ???? T2 a2 b0 e0 ? e1 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A b2. + ∀e2:a href="cic:/matita/basics/logic/R2.def(3)"R2/a ???? T2 a2 b0 e0 ? e1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b2. T3 b0 e0 b1 e1 b2 e2. #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2 -@(A href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/A ????? e2) -@(A href="cic:/matita/basics/logic/R2.def(3)"R2/A ?? ? ???? e0 ? e1) +@(a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/a ????? e2) +@(a href="cic:/matita/basics/logic/R2.def(3)"R2/a ?? ? ???? e0 ? e1) @a3 qed. definition R4 : ∀T0:Type[0]. ∀a0:T0. - ∀T1:∀x0:T0. A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A T0 a0 x0 → Type[0]. - ∀a1:T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0). - ∀T2:∀x0:T0. ∀p0:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T0 …) a0 x0. ∀x1:T1 x0 p0.A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T1 …) (A href="cic:/matita/basics/logic/R1.def(2)"R1/A T0 a0 T1 a1 x0 p0) x1 → Type[0]. - ∀a2:T2 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0)) a1). - ∀T3:∀x0:T0. ∀p0:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T1 …) (A href="cic:/matita/basics/logic/R1.def(2)"R1/A T0 a0 T1 a1 x0 p0) x1. - ∀x2:T2 x0 p0 x1 p1.A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T2 …) (A href="cic:/matita/basics/logic/R2.def(3)"R2/A T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0]. - ∀a3:T3 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0)) a1) - a2 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T2 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0)) a1)) a2). - ∀T4:∀x0:T0. ∀p0:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T1 …) (A href="cic:/matita/basics/logic/R1.def(2)"R1/A T0 a0 T1 a1 x0 p0) x1. - ∀x2:T2 x0 p0 x1 p1.∀p2:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T2 …) (A href="cic:/matita/basics/logic/R2.def(3)"R2/A T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2. - ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T3 …) (A href="cic:/matita/basics/logic/R3.def(4)"R3/A T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3. + ∀T1:∀x0:T0. a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a T0 a0 x0 → Type[0]. + ∀a1:T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0). + ∀T2:∀x0:T0. ∀p0:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T0 …) a0 x0. ∀x1:T1 x0 p0.a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T1 …) (a href="cic:/matita/basics/logic/R1.def(2)"R1/a T0 a0 T1 a1 x0 p0) x1 → Type[0]. + ∀a2:T2 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1). + ∀T3:∀x0:T0. ∀p0:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T1 …) (a href="cic:/matita/basics/logic/R1.def(2)"R1/a T0 a0 T1 a1 x0 p0) x1. + ∀x2:T2 x0 p0 x1 p1.a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T2 …) (a href="cic:/matita/basics/logic/R2.def(3)"R2/a T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0]. + ∀a3:T3 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1) + a2 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T2 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1)) a2). + ∀T4:∀x0:T0. ∀p0:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T1 …) (a href="cic:/matita/basics/logic/R1.def(2)"R1/a T0 a0 T1 a1 x0 p0) x1. + ∀x2:T2 x0 p0 x1 p1.∀p2:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T2 …) (a href="cic:/matita/basics/logic/R2.def(3)"R2/a T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2. + ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T3 …) (a href="cic:/matita/basics/logic/R3.def(4)"R3/a T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3. Type[0]. - ∀a4:T4 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0)) a1) - a2 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T2 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0)) a1)) a2) - a3 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T3 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0)) a1) - a2 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T2 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0)) a1)) a2)) + ∀a4:T4 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1) + a2 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T2 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1)) a2) + a3 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T3 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1) + a2 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T2 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1)) a2)) a3). ∀b0:T0. - ∀e0:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T0 …) a0 b0. + ∀e0:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T0 …) a0 b0. ∀b1: T1 b0 e0. - ∀e1:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T1 …) (A href="cic:/matita/basics/logic/R1.def(2)"R1/A T0 a0 T1 a1 b0 e0) b1. + ∀e1:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T1 …) (a href="cic:/matita/basics/logic/R1.def(2)"R1/a T0 a0 T1 a1 b0 e0) b1. ∀b2: T2 b0 e0 b1 e1. - ∀e2:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T2 …) (A href="cic:/matita/basics/logic/R2.def(3)"R2/A T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2. + ∀e2:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T2 …) (a href="cic:/matita/basics/logic/R2.def(3)"R2/a T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2. ∀b3: T3 b0 e0 b1 e1 b2 e2. - ∀e3:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T3 …) (A href="cic:/matita/basics/logic/R3.def(4)"R3/A T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3. + ∀e3:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T3 …) (a href="cic:/matita/basics/logic/R3.def(4)"R3/a T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3. T4 b0 e0 b1 e1 b2 e2 b3 e3. #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3 -@(A href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/A ????? e3) -@(A href="cic:/matita/basics/logic/R3.def(4)"R3/A ????????? e0 ? e1 ? e2) +@(a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/a ????? e3) +@(a href="cic:/matita/basics/logic/R3.def(4)"R3/a ????????? e0 ? e1 ? e2) @a4 qed. (* TODO concrete definition by means of proof irrelevance *) -axiom streicherK : ∀T:Type[1].∀t:T.∀P:t A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A t → Type[2].P (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? t) → ∀p.P p. +axiom streicherK : ∀T:Type[1].∀t:T.∀P:t a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a t → Type[2].P (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? t) → ∀p.P p. + -- 2.39.2