X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Flogic.ma;h=ffe1498f5a95fdbdc6e751b05fd123b5009e0740;hb=829e3a8af3229c4e625245f7265dd67939da98c4;hp=aeee17a7323f3f4abda175fde73c01229d6a0866;hpb=f1ef0a9e283af00cace679efd5775062c2a8f05c;p=helm.git

diff --git a/weblib/basics/logic.ma b/weblib/basics/logic.ma
index aeee17a73..ffe1498f5 100644
--- 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 ≝
+img class="anchor" src="icons/tick.png" id="eq"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: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.
+img class="anchor" src="icons/tick.png" id="eq_rect_r"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. a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a → Type[3]. 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.
+img class="anchor" src="icons/tick.png" id="eq_ind_r"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.
 
-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 #H #x #p (generalize in match H) (generalize in match P)
+img class="anchor" src="icons/tick.png" id="eq_rect_Type0_r"lemma eq_rect_Type0_r:
+  ∀A.∀a.∀P: ∀x:A. a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a → Type[0]. 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 lapply H lapply P
+  cases p; //; qed.
+
+img class="anchor" src="icons/tick.png" id="eq_rect_Type1_r"lemma eq_rect_Type1_r:
+  ∀A.∀a.∀P: ∀x:A. a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a → Type[1]. 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 lapply H lapply P
+  cases p; //; qed.
+
+img class="anchor" src="icons/tick.png" id="eq_rect_Type2_r"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 #H #x #p lapply H lapply P
+  cases p; //; qed.
+
+img class="anchor" src="icons/tick.png" id="eq_rect_Type3_r"lemma eq_rect_Type3_r:
+  ∀A.∀a.∀P: ∀x:A. a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a → Type[3]. 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 lapply H lapply 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.
+img class="anchor" src="icons/tick.png" id="rewrite_l"theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Type[2]. 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.
+img class="anchor" src="icons/tick.png" id="sym_eq"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.
+img class="anchor" src="icons/tick.png" id="rewrite_r"theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Type[2]. 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.
+img class="anchor" src="icons/tick.png" id="eq_coerc"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.
+img class="anchor" src="icons/tick.png" id="trans_eq"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.
+img class="anchor" src="icons/tick.png" id="eq_f"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.
+img class="anchor" src="icons/tick.png" id="eq_f2"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.
 #A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed. 
 
+img class="anchor" src="icons/tick.png" id="eq_f3"lemma eq_f3: ∀A,B,C,D.∀f:A→B→C->D.
+∀x1,x2:A.∀y1,y2:B. ∀z1,z2:C. x1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax2 → y1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ay2 → z1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/az2 → f x1 y1 z1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 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.
@@ -71,102 +88,102 @@ unification hint 0 ≔ T,a,b;
   
 (********** connectives ********)
 
-inductive True: Prop ≝  
+img class="anchor" src="icons/tick.png" id="True"inductive True: Prop ≝  
 I : True.
 
-inductive False: Prop ≝ .
+img class="anchor" src="icons/tick.png" id="False"inductive False: Prop ≝ .
 
 (* ndefinition Not: Prop → Prop ≝
 λA. A → False. *)
 
-inductive Not (A:Prop): Prop ≝
+img class="anchor" src="icons/tick.png" id="Not"inductive Not (A:Prop): Prop ≝
 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.
-#A #H #Hn (elim Hn); /2/; qed.
+img class="anchor" src="icons/tick.png" id="absurd"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); /span class="autotactic"2span class="autotrace" trace /span/span/; qed.
 
 (*
 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.
-/4/; qed.
+img class="anchor" src="icons/tick.png" id="not_to_not"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.
+/span class="autotactic"4span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a, a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a/span/span/; 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.
-/3/; qed.
+img class="anchor" src="icons/tick.png" id="sym_not_eq"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.
+/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a, a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a/span/span/; qed.
 
 (* and *)
-inductive And (A,B:Prop) : Prop ≝
+img class="anchor" src="icons/tick.png" id="And"inductive And (A,B:Prop) : Prop ≝
     conj : A → B → And A B.
 
 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.
+img class="anchor" src="icons/tick.png" id="proj1"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.
+img class="anchor" src="icons/tick.png" id="proj2"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 *)
-inductive Or (A,B:Prop) : Prop ≝
+img class="anchor" src="icons/tick.png" id="Or"inductive Or (A,B:Prop) : Prop ≝
      or_introl : A → (Or A B)
    | or_intror : B → (Or A B).
 
 interpretation "logical or" 'or x y = (Or x y).
 
-definition decidable : Prop → Prop ≝ 
+img class="anchor" src="icons/tick.png" id="decidable"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.
 
 (* exists *)
-inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
+img class="anchor" src="icons/tick.png" id="ex"inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
     ex_intro: ∀ x:A. P x →  ex A P.
     
 interpretation "exists" 'exists x = (ex ? x).
 
-inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝
+img class="anchor" src="icons/tick.png" id="ex2"inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝
     ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q.
 
 (* iff *)
-definition iff :=
+img class="anchor" src="icons/tick.png" id="iff"definition iff :=
  λ A,B. (A → B) a title="logical and" href="cic:/fakeuri.def(1)"∧/a (B → A).
 
 interpretation "iff" 'iff a b = (iff a b).
-  
-lemma iff_sym: ∀A,B. A ↔ B → B ↔ A.
-#A #B * /3/ qed.
 
-lemma iff_trans:∀A,B,C. A ↔ B → B ↔ C → A ↔ C.
-#A #B #C * #H1 #H2 * #H3 #H4 % /3/ qed.
+img class="anchor" src="icons/tick.png" id="iff_sym"lemma iff_sym: ∀A,B. A a title="iff" href="cic:/fakeuri.def(1)"↔/a B → B a title="iff" href="cic:/fakeuri.def(1)"↔/a A.
+#A #B * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ qed.
+
+img class="anchor" src="icons/tick.png" id="iff_trans"lemma iff_trans:∀A,B,C. A a title="iff" href="cic:/fakeuri.def(1)"↔/a B → B a title="iff" href="cic:/fakeuri.def(1)"↔/a C → A a title="iff" href="cic:/fakeuri.def(1)"↔/a C.
+#A #B #C * #H1 #H2 * #H3 #H4 % /span class="autotactic"3span class="autotrace" trace /span/span/ qed.
+
+img class="anchor" src="icons/tick.png" id="iff_not"lemma iff_not: ∀A,B. A a title="iff" href="cic:/fakeuri.def(1)"↔/a B → a title="logical not" href="cic:/fakeuri.def(1)"¬/aA a title="iff" href="cic:/fakeuri.def(1)"↔/a a title="logical not" href="cic:/fakeuri.def(1)"¬/aB.
+#A #B * #H1 #H2 % /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a/span/span/ qed.
 
-lemma iff_not: ∀A,B. A ↔ B → ¬A ↔ ¬B.
-#A #B * #H1 #H2 % /3/ qed.
+img class="anchor" src="icons/tick.png" id="iff_and_l"lemma iff_and_l: ∀A,B,C. A a title="iff" href="cic:/fakeuri.def(1)"↔/a B → C a title="logical and" href="cic:/fakeuri.def(1)"∧/a A a title="iff" href="cic:/fakeuri.def(1)"↔/a C a title="logical and" href="cic:/fakeuri.def(1)"∧/a B.
+#A #B #C * #H1 #H2 % * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ qed.  
 
-lemma iff_and_l: ∀A,B,C. A ↔ B → C ∧ A ↔ C ∧ B.
-#A #B #C * #H1 #H2 % * /3/ qed.  
+img class="anchor" src="icons/tick.png" id="iff_and_r"lemma iff_and_r: ∀A,B,C. A a title="iff" href="cic:/fakeuri.def(1)"↔/a B → A a title="logical and" href="cic:/fakeuri.def(1)"∧/a C a title="iff" href="cic:/fakeuri.def(1)"↔/a B a title="logical and" href="cic:/fakeuri.def(1)"∧/a C.
+#A #B #C * #H1 #H2 % * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ qed.  
 
-lemma iff_and_r: ∀A,B,C. A ↔ B → A ∧ C ↔ B ∧ C.
-#A #B #C * #H1 #H2 % * /3/ qed.  
+img class="anchor" src="icons/tick.png" id="iff_or_l"lemma iff_or_l: ∀A,B,C. A a title="iff" href="cic:/fakeuri.def(1)"↔/a B → C a title="logical or" href="cic:/fakeuri.def(1)"∨/a A a title="iff" href="cic:/fakeuri.def(1)"↔/a C a title="logical or" href="cic:/fakeuri.def(1)"∨/a B.
+#A #B #C * #H1 #H2 % * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ qed.  
 
-lemma iff_or_l: ∀A,B,C. A ↔ B → C ∨ A ↔ C ∨ B.
-#A #B #C * #H1 #H2 % * /3/ qed.  
+img class="anchor" src="icons/tick.png" id="iff_or_r"lemma iff_or_r: ∀A,B,C. A a title="iff" href="cic:/fakeuri.def(1)"↔/a B → A a title="logical or" href="cic:/fakeuri.def(1)"∨/a C a title="iff" href="cic:/fakeuri.def(1)"↔/a B a title="logical or" href="cic:/fakeuri.def(1)"∨/a C.
+#A #B #C * #H1 #H2 % * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ qed.  
 
-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.
+img class="anchor" src="icons/tick.png" id="R0"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.
+img class="anchor" src="icons/tick.png" id="R1"definition R1 ≝ a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/a.
 
-(* useless stuff *)
-definition R2 :
+(* used for lambda-delta *)
+img class="anchor" src="icons/tick.png" id="R2"definition R2 :
   ∀T0:Type[0].
   ∀a0:T0.
   ∀T1:∀x0:T0. a0a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax0 → Type[0].
@@ -184,7 +201,7 @@ definition R2 :
 @a2 
 qed.
 
-definition R3 :
+img class="anchor" src="icons/tick.png" id="R3"definition R3 :
   ∀T0:Type[0].
   ∀a0:T0.
   ∀T1:∀x0:T0. a0a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax0 → Type[0].
@@ -207,7 +224,7 @@ definition R3 :
 @a3 
 qed.
 
-definition R4 :
+img class="anchor" src="icons/tick.png" id="R4"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].
@@ -238,9 +255,18 @@ definition R4 :
   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/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.
\ No newline at end of file
+img class="anchor" src="icons/tick.png" id="eqProp"definition eqProp ≝ λA:Prop.a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a A.
+
+(* Example to avoid indexing and the consequential creation of ill typed
+   terms during paramodulation *)
+img class="anchor" src="icons/tick.png" id="lemmaK"example lemmaK : ∀A.∀x:A.∀h:xa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax. a href="cic:/matita/basics/logic/eqProp.def(1)"eqProp/a ? h (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a A x).
+#A #x #h @(a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? h: a href="cic:/matita/basics/logic/eqProp.def(1)"eqProp/a ? ? ?).
+qed.
+
+img class="anchor" src="icons/tick.png" id="streicherK"theorem streicherK : ∀T:Type[2].∀t:T.∀P:t a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a t → Type[3].P (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? t) → ∀p.P p.
+ #T #t #P #H #p >(a href="cic:/matita/basics/logic/lemmaK.def(2)"lemmaK/a T t p) @H
+qed.