manual commit after active hyperlinks

[helm.git] / weblib / basics / logic.ma

diff --git a/weblib/basics/logic.ma b/weblib/basics/logic.ma
index 527e48429836af118c8f812430b6e2e95e6fe855..ffe1498f5a95fdbdc6e751b05fd123b5009e0740 100644 (file)
--- a/weblib/basics/logic.ma
+++ b/weblib/basics/logic.ma
@@ -14,64 +14,64 @@ include "hints_declaration.ma".
 
 (* propositional equality *)
 
-inductive eq (A:Type[2]) (x:A) : A → Prop ≝
+\ 5img class="anchor" src="icons/tick.png" id="eq"\ 6inductive 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:
+\ 5img class="anchor" src="icons/tick.png" id="eq_rect_r"\ 6lemma 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. \ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a → Type[3]. 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 (cases p) // qed.
 
-lemma eq_ind_r :
+\ 5img class="anchor" src="icons/tick.png" id="eq_ind_r"\ 6lemma 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.
 
-lemma eq_rect_Type0_r:
+\ 5img class="anchor" src="icons/tick.png" id="eq_rect_Type0_r"\ 6lemma eq_rect_Type0_r:
   ∀A.∀a.∀P: ∀x:A. \ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a → Type[0]. 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 lapply H lapply P
   cases p; //; qed.
 
-lemma eq_rect_Type1_r:
+\ 5img class="anchor" src="icons/tick.png" id="eq_rect_Type1_r"\ 6lemma eq_rect_Type1_r:
   ∀A.∀a.∀P: ∀x:A. \ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a → Type[1]. 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 lapply H lapply P
   cases p; //; qed.
 
-lemma eq_rect_Type2_r:
+\ 5img class="anchor" src="icons/tick.png" id="eq_rect_Type2_r"\ 6lemma 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 lapply H lapply P
   cases p; //; qed.
 
-lemma eq_rect_Type3_r:
+\ 5img class="anchor" src="icons/tick.png" id="eq_rect_Type3_r"\ 6lemma eq_rect_Type3_r:
   ∀A.∀a.∀P: ∀x:A. \ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 ? x a → Type[3]. 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 lapply H lapply P
   cases p; //; qed.
 
-theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y → P y.
+\ 5img class="anchor" src="icons/tick.png" id="rewrite_l"\ 6theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 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.
+\ 5img class="anchor" src="icons/tick.png" id="sym_eq"\ 6theorem 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 rewrite_r: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x → P y.
+\ 5img class="anchor" src="icons/tick.png" id="rewrite_r"\ 6theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Type[2]. 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 eq_coerc: ∀A,B:Type[0].A→(A\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6B)→B.
+\ 5img class="anchor" src="icons/tick.png" id="eq_coerc"\ 6theorem eq_coerc: ∀A,B:Type[0].A→(A\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6B)→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.
+\ 5img class="anchor" src="icons/tick.png" id="trans_eq"\ 6theorem 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.
 #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.
+\ 5img class="anchor" src="icons/tick.png" id="eq_f"\ 6theorem 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.
 #A #B #f #x #y #H >H; //; qed.
 
 (* deleterio per auto? *)
-theorem eq_f2: ∀A,B,C.∀f:A→B→C.
+\ 5img class="anchor" src="icons/tick.png" id="eq_f2"\ 6theorem 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.
 #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.
+\ 5img class="anchor" src="icons/tick.png" id="eq_f3"\ 6lemma eq_f3: ∀A,B,C,D.∀f:A→B→C->D.
 ∀x1,x2:A.∀y1,y2:B. ∀z1,z2:C. 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 → z1\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6z2 → f x1 y1 z1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x2 y2 z2.
 #A #B #C #D #f #x1 #x2 #y1 #y2 #z1 #z2 #E1 #E2 #E3 >E1; >E2; >E3 //; qed.
 
@@ -88,20 +88,20 @@ unification hint 0 ≔ T,a,b;
   
 (********** connectives ********)
 
-inductive True: Prop ≝  
+\ 5img class="anchor" src="icons/tick.png" id="True"\ 6inductive True: Prop ≝  
 I : True.
 
-inductive False: Prop ≝ .
+\ 5img class="anchor" src="icons/tick.png" id="False"\ 6inductive False: Prop ≝ .
 
 (* ndefinition Not: Prop → Prop ≝
 λA. A → False. *)
 
-inductive Not (A:Prop): Prop ≝
+\ 5img class="anchor" src="icons/tick.png" id="Not"\ 6inductive Not (A:Prop): Prop ≝
 nmk: (A → \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6) → 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.
+\ 5img class="anchor" src="icons/tick.png" id="absurd"\ 6theorem 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.
 #A #H #Hn (elim Hn); /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/; qed.
 
 (*
@@ -109,81 +109,81 @@ 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.
+\ 5img class="anchor" src="icons/tick.png" id="not_to_not"\ 6theorem 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.
 /\ 5span class="autotactic"\ 64\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/; 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.
+\ 5img class="anchor" src="icons/tick.png" id="sym_not_eq"\ 6theorem 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.
 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/; qed.
 
 (* and *)
-inductive And (A,B:Prop) : Prop ≝
+\ 5img class="anchor" src="icons/tick.png" id="And"\ 6inductive 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 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 B → A.
+\ 5img class="anchor" src="icons/tick.png" id="proj1"\ 6theorem proj1: ∀A,B:Prop. A \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 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.
+\ 5img class="anchor" src="icons/tick.png" id="proj2"\ 6theorem proj2: ∀ A,B:Prop. A \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 B → B.
 #A #B #AB (elim AB) //; qed.
 
 (* or *)
-inductive Or (A,B:Prop) : Prop ≝
+\ 5img class="anchor" src="icons/tick.png" id="Or"\ 6inductive 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 ≝ 
+\ 5img class="anchor" src="icons/tick.png" id="decidable"\ 6definition 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.
 
 (* exists *)
-inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
+\ 5img class="anchor" src="icons/tick.png" id="ex"\ 6inductive 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 ≝
+\ 5img class="anchor" src="icons/tick.png" id="ex2"\ 6inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝
     ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q.
 
 (* iff *)
-definition iff :=
+\ 5img class="anchor" src="icons/tick.png" id="iff"\ 6definition iff :=
  λ A,B. (A → B) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 (B → A).
 
 interpretation "iff" 'iff a b = (iff a b).
 
-lemma iff_sym: ∀A,B. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → B \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 A.
+\ 5img class="anchor" src="icons/tick.png" id="iff_sym"\ 6lemma iff_sym: ∀A,B. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → B \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 A.
 #A #B * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
 
-lemma iff_trans:∀A,B,C. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → B \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 C → A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 C.
+\ 5img class="anchor" src="icons/tick.png" id="iff_trans"\ 6lemma iff_trans:∀A,B,C. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → B \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 C → A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 C.
 #A #B #C * #H1 #H2 * #H3 #H4 % /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ qed.
 
-lemma iff_not: ∀A,B. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6B.
+\ 5img class="anchor" src="icons/tick.png" id="iff_not"\ 6lemma iff_not: ∀A,B. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6B.
 #A #B * #H1 #H2 % /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
 
-lemma iff_and_l: ∀A,B,C. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → C \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 C \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 B.
+\ 5img class="anchor" src="icons/tick.png" id="iff_and_l"\ 6lemma iff_and_l: ∀A,B,C. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → C \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 C \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 B.
 #A #B #C * #H1 #H2 % * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.  
 
-lemma iff_and_r: ∀A,B,C. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → A \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 C \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 C.
+\ 5img class="anchor" src="icons/tick.png" id="iff_and_r"\ 6lemma iff_and_r: ∀A,B,C. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → A \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 C \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 C.
 #A #B #C * #H1 #H2 % * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.  
 
-lemma iff_or_l: ∀A,B,C. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → C \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 C \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 B.
+\ 5img class="anchor" src="icons/tick.png" id="iff_or_l"\ 6lemma iff_or_l: ∀A,B,C. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → C \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 C \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 B.
 #A #B #C * #H1 #H2 % * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.  
 
-lemma iff_or_r: ∀A,B,C. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → A \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 C \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 C.
+\ 5img class="anchor" src="icons/tick.png" id="iff_or_r"\ 6lemma iff_or_r: ∀A,B,C. A \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B → A \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 C \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 B \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 C.
 #A #B #C * #H1 #H2 % * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.  
 
 (* cose per destruct: da rivedere *) 
 
-definition R0 ≝ λT:Type[0].λt:T.t.
+\ 5img class="anchor" src="icons/tick.png" id="R0"\ 6definition 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.
+\ 5img class="anchor" src="icons/tick.png" id="R1"\ 6definition R1 ≝ \ 5a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"\ 6eq_rect_Type0\ 5/a\ 6.
 
 (* used for lambda-delta *)
-definition R2 :
+\ 5img class="anchor" src="icons/tick.png" id="R2"\ 6definition 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].
@@ -201,7 +201,7 @@ definition R2 :
 @a2 
 qed.
 
-definition R3 :
+\ 5img class="anchor" src="icons/tick.png" id="R3"\ 6definition 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].
@@ -224,7 +224,7 @@ definition R3 :
 @a3 
 qed.
 
-definition R4 :
+\ 5img class="anchor" src="icons/tick.png" id="R4"\ 6definition 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].
@@ -259,14 +259,14 @@ definition R4 :
 @a4 
 qed.
 
-definition eqProp ≝ λA:Prop.\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 A.
+\ 5img class="anchor" src="icons/tick.png" id="eqProp"\ 6definition eqProp ≝ λA:Prop.\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 A.
 
 (* Example to avoid indexing and the consequential creation of ill typed
    terms during paramodulation *)
-example lemmaK : ∀A.∀x:A.∀h:x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x. \ 5a href="cic:/matita/basics/logic/eqProp.def(1)"\ 6eqProp\ 5/a\ 6 ? h (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 A x).
+\ 5img class="anchor" src="icons/tick.png" id="lemmaK"\ 6example lemmaK : ∀A.∀x:A.∀h:x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x. \ 5a href="cic:/matita/basics/logic/eqProp.def(1)"\ 6eqProp\ 5/a\ 6 ? h (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 A x).
 #A #x #h @(\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? h: \ 5a href="cic:/matita/basics/logic/eqProp.def(1)"\ 6eqProp\ 5/a\ 6 ? ? ?).
 qed.
 
-theorem streicherK : ∀T:Type[2].∀t:T.∀P:t \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 t → Type[3].P (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? t) → ∀p.P p.
+\ 5img class="anchor" src="icons/tick.png" id="streicherK"\ 6theorem streicherK : ∀T:Type[2].∀t:T.∀P:t \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 t → Type[3].P (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? t) → ∀p.P p.
  #T #t #P #H #p >(\ 5a href="cic:/matita/basics/logic/lemmaK.def(2)"\ 6lemmaK\ 5/a\ 6 T t p) @H
 qed.