commit by user andrea

diff --git a/weblib/basics/logic.ma b/weblib/basics/logic.ma
index aeee17a7323f3f4abda175fde73c01229d6a0866..8f981d46924556ee885407a1320d147ef07aaad0 100644 (file)
--- a/weblib/basics/logic.ma
+++ b/weblib/basics/logic.ma
@@ -1,4 +1,4 @@
-(*
+ (*
     ||M||  This file is part of HELM, an Hypertextual, Electronic        
     ||A||  Library of Mathematics, developed at the Computer Science     
     ||T||  Department of the University of Bologna, Italy.                     
@@ -10,54 +10,71 @@
       V_______________________________________________________________ *)
 
 include "basics/pts.ma".
-(*include "hints_declaration.ma".*)
+include "hints_declaration.ma".
 
 (* propositional equality *)
 
-inductive eq (A:Type[1]) (x:A) : A → Prop ≝
+inductive eq (A:Type[2]) (x:A) : A → Prop ≝
     refl: eq A x x. 
-
+    
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
+interpretation "leibniz reflexivity" 'refl = refl.
 
 lemma eq_rect_r:
- ∀A.∀a,x.∀p:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a.∀P: 
- ∀x:A. x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a → Type[2]. P a (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 A a) → P x p.
+ ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[3]. P a (refl A a) → P x p.
  #A #a #x #p (cases p) // qed.
 
 lemma eq_ind_r :
- ∀A.∀a.∀P: ∀x:A. x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a → Prop. P a (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 A a) → 
-   ∀x.∀p:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a.P x p.
- #A #a #P #p #x0 #p0; @(\ 5a href="cic:/matita/basics/logic/eq_rect_r.def(1)"\ 6eq_rect_r\ 5/a\ 6 ? ? ? p0) //; qed.
+ ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A #a #P #p #x0 #p0; @(eq_rect_r ? ? ? p0) //; qed.
+
+lemma eq_rect_Type0_r:
+  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+  #A #a #P #H #x #p lapply H lapply P
+  cases p; //; qed.
+
+lemma eq_rect_Type1_r:
+  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+  #A #a #P #H #x #p lapply H lapply P
+  cases p; //; qed.
 
 lemma eq_rect_Type2_r:
-  ∀A.∀a.∀P: ∀x:A. \ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a → Type[2]. P a (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 A a) → 
-    ∀x.∀p:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a.P x p.
-  #A #a #P #H #x #p (generalize in match H) (generalize in match P)
+  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+  #A #a #P #H #x #p lapply H lapply P
+  cases p; //; qed.
+
+lemma eq_rect_Type3_r:
+  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[3]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+  #A #a #P #H #x #p lapply H lapply P
   cases p; //; qed.
 
-theorem rewrite_l: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y → P y.
+theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. x = y → P y.
 #A #x #P #Hx #y #Heq (cases Heq); //; qed.
 
-theorem sym_eq: ∀A.∀x,y:A. x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y → y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x.
-#A #x #y #Heq @(\ 5a href="cic:/matita/basics/logic/rewrite_l.def(1)"\ 6rewrite_l\ 5/a\ 6 A x (λz.z\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x)); //; qed.
+theorem sym_eq: ∀A.∀x,y:A. x = y → y = x.
+#A #x #y #Heq @(rewrite_l A x (λz.z=x)) // qed.
 
-theorem rewrite_r: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x → P y.
-#A #x #P #Hx #y #Heq (cases (\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 ? ? ? Heq)); //; qed.
+theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. y = x → P y.
+#A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed.
 
-theorem eq_coerc: ∀A,B:Type[0].A→(A\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6B)→B.
+theorem eq_coerc: ∀A,B:Type[0].A→(A=B)→B.
 #A #B #Ha #Heq (elim Heq); //; qed.
 
-theorem trans_eq : ∀A.∀x,y,z:A. x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y → y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 z → x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 z.
+theorem trans_eq : ∀A.∀x,y,z:A. x = y → y = z → x = z.
 #A #x #y #z #H1 #H2 >H1; //; qed.
 
-theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6y → f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f y.
+theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. x=y → f x = 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. x1\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x2 → y1\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6y2 → f x1 y1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x2 y2.
+∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
 #A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed. 
 
+lemma eq_f3: ∀A,B,C,D.∀f:A→B→C->D.
+∀x1,x2:A.∀y1,y2:B. ∀z1,z2:C. x1=x2 → y1=y2 → z1=z2 → f x1 y1 z1 = f x2 y2 z2.
+#A #B #C #D #f #x1 #x2 #y1 #y2 #z1 #z2 #E1 #E2 #E3 >E1; >E2; >E3 //; qed.
+
 (* hint to genereric equality 
 definition eq_equality: equality ≝
  mk_equality eq refl rewrite_l rewrite_r.
@@ -80,12 +97,11 @@ inductive False: Prop ≝ .
 λA. A → False. *)
 
 inductive Not (A:Prop): Prop ≝
-nmk: (A → \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6) → Not A.
-
+nmk: (A → False) → Not A.
 
 interpretation "logical not" 'not x = (Not x).
 
-theorem absurd : ∀A:Prop. A → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6A → \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6.
+theorem absurd : ∀A:Prop. A → ¬A → False.
 #A #H #Hn (elim Hn); /2/; qed.
 
 (*
@@ -93,13 +109,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) → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6B →\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6A.
+theorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
 /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 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 y → y \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 x.
+theorem sym_not_eq: ∀A.∀x,y:A. x ≠ y → y ≠ x.
 /3/; qed.
 
 (* and *)
@@ -108,10 +124,10 @@ inductive And (A,B:Prop) : Prop ≝
 
 interpretation "logical and" 'and x y = (And x y).
 
-theorem proj1: ∀A,B:Prop. A \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 B → A.
+theorem proj1: ∀A,B:Prop. A ∧ B → A.
 #A #B #AB (elim AB) //; qed.
 
-theorem proj2: ∀ A,B:Prop. A \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 B → B.
+theorem proj2: ∀ A,B:Prop. A ∧ B → B.
 #A #B #AB (elim AB) //; qed.
 
 (* or *)
@@ -122,7 +138,7 @@ inductive Or (A,B:Prop) : Prop ≝
 interpretation "logical or" 'or x y = (Or x y).
 
 definition decidable : Prop → Prop ≝ 
-λ A:Prop. A \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 A.
+λ A:Prop. A ∨ ¬ A.
 
 (* exists *)
 inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
@@ -135,10 +151,10 @@ inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝
 
 (* iff *)
 definition iff :=
- λ A,B. (A → B) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 (B → A).
+ λ A,B. (A → B) ∧ (B → A).
 
 interpretation "iff" 'iff a b = (iff a b).
-  
+
 lemma iff_sym: ∀A,B. A ↔ B → B ↔ A.
 #A #B * /3/ qed.
 
@@ -159,88 +175,98 @@ lemma iff_or_l: ∀A,B,C. A ↔ B → C ∨ A ↔ C ∨ B.
 
 lemma iff_or_r: ∀A,B,C. A ↔ B → A ∨ C ↔ B ∨ C.
 #A #B #C * #H1 #H2 % * /3/ qed.  
+
 (* cose per destruct: da rivedere *) 
 
 definition R0 ≝ λT:Type[0].λt:T.t.
   
-definition R1 ≝ \ 5a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"\ 6eq_rect_Type0\ 5/a\ 6.
+definition R1 ≝ eq_rect_Type0.
 
-(* useless stuff *)
+(* used for lambda-delta *)
 definition R2 :
   ∀T0:Type[0].
   ∀a0:T0.
-  ∀T1:∀x0:T0. a0\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x0 → Type[0].
-  ∀a1:T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? a0).
-  ∀T2:∀x0:T0. ∀p0:a0\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x0. ∀x1:T1 x0 p0. \ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 ?? T1 a1 ? p0 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x1 → Type[0].
-  ∀a2:T2 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? a1).
+  ∀T1:∀x0:T0. a0=x0 → Type[0].
+  ∀a1:T1 a0 (refl ? a0).
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
+  ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
   ∀b0:T0.
-  ∀e0:a0 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b0.
+  ∀e0:a0 = b0.
   ∀b1: T1 b0 e0.
-  ∀e1:\ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 ?? T1 a1 ? e0 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b1.
+  ∀e1:R1 ?? T1 a1 ? e0 = b1.
   T2 b0 e0 b1 e1.
 #T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1 
-@(\ 5a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"\ 6eq_rect_Type0\ 5/a\ 6 ????? e1) 
-@(\ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 ?? ? ?? e0) 
+@(eq_rect_Type0 ????? e1) 
+@(R1 ?? ? ?? e0) 
 @a2 
 qed.
 
 definition R3 :
   ∀T0:Type[0].
   ∀a0:T0.
-  ∀T1:∀x0:T0. a0\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x0 → Type[0].
-  ∀a1:T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? a0).
-  ∀T2:∀x0:T0. ∀p0:a0\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x0. ∀x1:T1 x0 p0. \ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 ?? T1 a1 ? p0 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x1 → Type[0].
-  ∀a2:T2 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? a1).
-  ∀T3:∀x0:T0. ∀p0:a0\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x0. ∀x1:T1 x0 p0.∀p1:\ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 ?? T1 a1 ? p0 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x1.
-      ∀x2:T2 x0 p0 x1 p1.\ 5a href="cic:/matita/basics/logic/R2.def(3)"\ 6R2\ 5/a\ 6 ???? T2 a2 x0 p0 ? p1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x2 → Type[0].
-  ∀a3:T3 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? a1) a2 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? a2).
+  ∀T1:∀x0:T0. a0=x0 → Type[0].
+  ∀a1:T1 a0 (refl ? a0).
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
+  ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
+  ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
+      ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
+  ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
   ∀b0:T0.
-  ∀e0:a0 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b0.
+  ∀e0:a0 = b0.
   ∀b1: T1 b0 e0.
-  ∀e1:\ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 ?? T1 a1 ? e0 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b1.
+  ∀e1:R1 ?? T1 a1 ? e0 = b1.
   ∀b2: T2 b0 e0 b1 e1.
-  ∀e2:\ 5a href="cic:/matita/basics/logic/R2.def(3)"\ 6R2\ 5/a\ 6 ???? T2 a2 b0 e0 ? e1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b2.
+  ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
   T3 b0 e0 b1 e1 b2 e2.
 #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2 
-@(\ 5a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"\ 6eq_rect_Type0\ 5/a\ 6 ????? e2) 
-@(\ 5a href="cic:/matita/basics/logic/R2.def(3)"\ 6R2\ 5/a\ 6 ?? ? ???? e0 ? e1) 
+@(eq_rect_Type0 ????? e2) 
+@(R2 ?? ? ???? e0 ? e1) 
 @a3 
 qed.
 
 definition R4 :
   ∀T0:Type[0].
   ∀a0:T0.
-  ∀T1:∀x0:T0. \ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 T0 a0 x0 → Type[0].
-  ∀a1:T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0).
-  ∀T2:∀x0:T0. ∀p0:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T0 …) a0 x0. ∀x1:T1 x0 p0.\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T1 …) (\ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 T0 a0 T1 a1 x0 p0) x1 → Type[0].
-  ∀a2:T2 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0)) a1).
-  ∀T3:∀x0:T0. ∀p0:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T1 …) (\ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 T0 a0 T1 a1 x0 p0) x1.
-      ∀x2:T2 x0 p0 x1 p1.\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T2 …) (\ 5a href="cic:/matita/basics/logic/R2.def(3)"\ 6R2\ 5/a\ 6 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
-  ∀a3:T3 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0)) a1) 
-      a2 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T2 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0)) a1)) a2). 
-  ∀T4:∀x0:T0. ∀p0:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T1 …) (\ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 T0 a0 T1 a1 x0 p0) x1.
-      ∀x2:T2 x0 p0 x1 p1.∀p2:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T2 …) (\ 5a href="cic:/matita/basics/logic/R2.def(3)"\ 6R2\ 5/a\ 6 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
-      ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T3 …) (\ 5a href="cic:/matita/basics/logic/R3.def(4)"\ 6R3\ 5/a\ 6 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3. 
+  ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
+  ∀a1:T1 a0 (refl T0 a0).
+  ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
+  ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
+  ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+      ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
+  ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1) 
+      a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2). 
+  ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+      ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
+      ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3. 
       Type[0].
-  ∀a4:T4 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0)) a1) 
-      a2 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T2 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0)) a1)) a2) 
-      a3 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T3 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0)) a1) 
-                   a2 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T2 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0) a1 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 (T1 a0 (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 T0 a0)) a1)) a2))
+  ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1) 
+      a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2) 
+      a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1) 
+                   a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
                    a3).
   ∀b0:T0.
-  ∀e0:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T0 …) a0 b0.
+  ∀e0:eq (T0 …) a0 b0.
   ∀b1: T1 b0 e0.
-  ∀e1:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T1 …) (\ 5a href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/a\ 6 T0 a0 T1 a1 b0 e0) b1.
+  ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
   ∀b2: T2 b0 e0 b1 e1.
-  ∀e2:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T2 …) (\ 5a href="cic:/matita/basics/logic/R2.def(3)"\ 6R2\ 5/a\ 6 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
+  ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
   ∀b3: T3 b0 e0 b1 e1 b2 e2.
-  ∀e3:\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 (T3 …) (\ 5a href="cic:/matita/basics/logic/R3.def(4)"\ 6R3\ 5/a\ 6 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
+  ∀e3:eq (T3 …) (R3 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 
-@(\ 5a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"\ 6eq_rect_Type0\ 5/a\ 6 ????? e3) 
-@(\ 5a href="cic:/matita/basics/logic/R3.def(4)"\ 6R3\ 5/a\ 6 ????????? e0 ? e1 ? e2)
+@(eq_rect_Type0 ????? e3) 
+@(R3 ????????? e0 ? e1 ? e2) 
 @a4 
 qed.
 
-(* TODO concrete definition by means of proof irrelevance *)
-axiom streicherK : ∀T:Type[1].∀t:T.∀P:t \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 t → Type[2].P (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? t) → ∀p.P p.
\ No newline at end of file
+definition eqProp ≝ λA:Prop.eq A.
+
+(* Example to avoid indexing and the consequential creation of ill typed
+   terms during paramodulation *)
+example lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
+#A #x #h @(refl ? h: eqProp ? ? ?).
+qed.
+
+theorem streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[3].P (refl ? t) → ∀p.P p.
+ #T #t #P #H #p >(lemmaK T t p) @H
+qed.

diff --git a/weblib/basics/pts.ma b/weblib/basics/pts.ma
index b7d9a5da9deb592e73670182de1459befd569321..c0ec34b71cf9d3a0d431a8153ad033ada3fcd67a 100644 (file)
--- a/weblib/basics/pts.ma
+++ b/weblib/basics/pts.ma
@@ -18,4 +18,5 @@ universe constraint Type[0] < Type[1].
 universe constraint Type[1] < Type[2].
 universe constraint Type[2] < Type[3].
 universe constraint Type[3] < Type[4].
-
+universe constraint Type[4] < Type[5].
+ 
\ No newline at end of file

diff --git a/weblib/basics/types.ma b/weblib/basics/types.ma
index 0fd4eb5886cb0d067459a47b9c5703c5b48e413e..586ce31ce7bb527d251d3d1a9ddf5704f9163a2a 100644 (file)
--- a/weblib/basics/types.ma
+++ b/weblib/basics/types.ma
@@ -58,4 +58,4 @@ inductive option (A:Type[0]) : Type[0] ≝
 inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝
   dp: ∀a:A.(f a)→Sig A f.
 
-interpretation "Sigma" 'sigma x = (Sig ? x).
+interpretation "Sigma" 'sigma x = (Sig ? x).
\ No newline at end of file

diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma
index b21fd3e1787add792e06acdb24dbf62c14dba2b0..9043bdad712795d8f6f76104e72d4dc6601a3455 100644 (file)
--- a/weblib/tutorial/chapter1.ma
+++ b/weblib/tutorial/chapter1.ma
@@ -243,7 +243,7 @@ need a few more applications to handle reachability, and side conditions.
 The magic number to let automation work is, in this case, 9.  *)
 
 lemma problem: \ 5a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"\ 6reachable\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/start.def(1)"\ 6start\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/end.def(1)"\ 6end\ 5/a\ 6.
-normalize /9/ qed. 
+normalize /\ 5span class="autotactic"\ 69\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"\ 6one\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"\ 6with_boat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"\ 6opposite_side\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"\ 6move_goat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/move.con(0,2,0)"\ 6move_wolf\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/move.con(0,3,0)"\ 6move_cabbage\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"\ 6move_boat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"\ 6east_west\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"\ 6west_east\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed. 
 
 (* Let us now try to derive the proof in a more interactive way. Of course, we
 expect to need several moves to transfer all items from a bank to the other, so 
@@ -304,7 +304,7 @@ requires /2/ since move_goat opens an additional subgoal. By applying "]" we
 refocus on the skipped goal, going back to a situation similar to the one we
 started with. *)
 
-  | /2/ ] 
+  | /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"\ 6move_goat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"\ 6east_west\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ ] 
 
 (* Let us perform the next step, namely moving back the boat, in a sligtly 
 different way. The more operation expects as second argument the new 
@@ -319,7 +319,7 @@ the system. *)
 trivial. We\ 5span style="font-family: Verdana,sans-serif;"\ 6 \ 5/span\ 6can just apply automation to all of them, and it will close the two
 trivial goals. *)
 
-/2/
+/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"\ 6opposite_side\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"\ 6move_boat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"\ 6east_west\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"\ 6west_east\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 
 (* Let us come to the next step, that consists in moving the wolf. Suppose that 
 instead of specifying the next intermediate state, we prefer to specify the next 
@@ -338,12 +338,12 @@ be arbitrary). The simplest way to proceed is to focus on the bank, that is
 the fourth subgoal, and explicitly instatiate it. Instead of repeatedly using "|",
 we can perform focusing by typing "4:" as described by the following command. *)
 
-[4: @\ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6] /2/
+[4: @\ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6] /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"\ 6with_boat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"\ 6east_west\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 
 (* Alternatively, we can directly instantiate the bank into the move. Let
 us complete the proof in this, very readable way. *)
 
-@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"\ 6move_goat\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 … )) /2/
-@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,3,0)"\ 6move_cabbage\ 5/a\ 6 ?? \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 … )) /2/
-@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"\ 6move_boat\ 5/a\ 6 ??? \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 … )) /2/
-@\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"\ 6one\ 5/a\ 6 /2/ qed.
\ No newline at end of file
+@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"\ 6move_goat\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 … )) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"\ 6with_boat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"\ 6west_east\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,3,0)"\ 6move_cabbage\ 5/a\ 6 ?? \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 … )) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"\ 6opposite_side\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"\ 6east_west\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"\ 6west_east\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"\ 6move_boat\ 5/a\ 6 ??? \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 … )) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"\ 6with_boat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"\ 6west_east\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+@\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"\ 6one\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"\ 6move_goat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"\ 6east_west\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
\ No newline at end of file

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index b358f823245894dc6803ce927dafbe7943013ed1..8457aa48473c75affa2f64983ceca88b1f2d8318 100644 (file)
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -1,44 +1,63 @@
+(* In this Chapter we shall develop a naif theory of sets represented as characteristic
+predicates over some universe \ 5code\ 6A\ 5/code\ 6, that is as objects of type A→Prop *)
+
 include "basics/logic.ma".
 
-(**** a subset of A is just an object of type A→Prop ****)
+(**** For instance the empty set is defined by the always function predicate *)
 
-definition empty_set ≝ λA:Type[0].λa:A.False.
+definition empty_set ≝ λA:Type[0].λa:A.\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6.
 notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
 interpretation "empty set" 'empty_set = (empty_set ?).
 
-definition singleton ≝ λA.λx,a:A.x=a.
+(* Similarly, a singleton set contaning containing an element a, is defined
+by by the characteristic function asserting equality with a *)
+
+definition singleton ≝ λA.λx,a:A.x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6a.
 (* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
 interpretation "singleton" 'singl x = (singleton ? x).
 
-definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a ∨ Q a.
+(* The operations of union, intersection, complement and substraction 
+are easily defined in terms of the propositional connectives of dijunction,
+conjunction and negation *)
+
+definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 Q a.
 interpretation "union" 'union a b = (union ? a b).
 
-definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a ∧ Q a.
+definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 Q a.
 interpretation "intersection" 'intersects a b = (intersection ? a b).
 
-definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
+definition complement ≝ λU:Type[0].λA:U → Prop.λw.\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 A w.
 interpretation "complement" 'not a = (complement ? a).
 
-definition substraction := λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
+definition substraction := λU:Type[0].λA,B:U → Prop.λw.A w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 B w.
 interpretation "substraction" 'minus a b = (substraction ? a b).
 
+(* Finally, we use implication to define the inclusion relation between
+sets *)
+
 definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
 interpretation "subset" 'subseteq a b = (subset ? a b).
 
-(* extensional equality *)
-definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
+(* Two sets are equals if and only if they have the same elements, that is,
+if the two characteristic functions are extensionally equivalent: *) 
+
+definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 Q a.
 notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
 
+(* This notion of equality is different from the intensional equality of
+fucntions, hence we have to prove the usual properties: *)
+
 lemma eqP_sym: ∀U.∀A,B:U →Prop. 
-  A =1 B → B =1 A.
+  A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 B → B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A.
 #U #A #B #eqAB #a @iff_sym @eqAB qed.
  
 lemma eqP_trans: ∀U.∀A,B,C:U →Prop. 
   A =1 B → B =1 C → A =1 C.
 #U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
 
-lemma eqP_union_r: ∀U.∀A,B,C:U →Prop. 
+(* For the same reason, we must also prove that all the operations we have
+ lemma eqP_union_r: ∀U.∀A,B,C:U →Prop. 
   A =1 C  → A ∪ B =1 C ∪ B.
 #U #A #B #C #eqAB #a @iff_or_r @eqAB qed.