X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Flist.ma;h=d542416c48c27885fb6e04d1df354e0b342f3ba0;hb=c0ac63fead67ea1902e3d923ce877a2779cf501e;hp=6dcc181f5d98c7b324c17a9a4bd2553579361072;hpb=7f6235dca57343e63217316b6415599daef7d4aa;p=helm.git

diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma
index 6dcc181f5..d542416c4 100644
--- a/weblib/basics/list.ma
+++ b/weblib/basics/list.ma
@@ -11,7 +11,7 @@
 
 include "arithmetics/nat.ma".
 
-inductive list (A:Type[0]) : Type[0] :=
+img class="anchor" src="icons/tick.png" id="list"inductive list (A:Type[0]) : Type[0] :=
   | nil: list A
   | cons: A -> list A -> list A.
 
@@ -30,12 +30,12 @@ notation "hvbox(l1 break @ l2)"
 interpretation "nil" 'nil = (nil ?).
 interpretation "cons" 'cons hd tl = (cons ? hd tl).
 
-definition not_nil: ∀A:Type[0].a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A → Prop ≝
+img class="anchor" src="icons/tick.png" id="not_nil"definition not_nil: ∀A:Type[0].a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A → Prop ≝
  λA.λl.match l with [ nil ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a | cons hd tl ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a ].
 
-theorem nil_cons:
-  ∀A:Type[0].∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀a:A. aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a [a title="nil" href="cic:/fakeuri.def(1)"]/a.
-  #A #l #a @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Heq (change with (a href="cic:/matita/basics/list/not_nil.def(1)"not_nil/a ? (a:a title="cons" href="cic:/fakeuri.def(1)":/al))) >Heq //
+img class="anchor" src="icons/tick.png" id="nil_cons"theorem nil_cons:
+  ∀A:Type[0].∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀a:A. aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a.
+  #A #l #a @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Heq (change with (a href="cic:/matita/basics/list/not_nil.def(1)"not_nil/a ? (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al))) >Heq //
 qed.
 
 (*
@@ -44,23 +44,23 @@ let rec id_list A (l: list A) on l :=
   [ nil => []
   | (cons hd tl) => hd :: id_list A tl ]. *)
 
-let rec append A (l1: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) l2 on l1 ≝ 
+img class="anchor" src="icons/tick.png" id="append"let rec append A (l1: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) l2 on l1 ≝ 
   match l1 with
   [ nil ⇒  l2
-  | cons hd tl ⇒  hd :a title="cons" href="cic:/fakeuri.def(1)":/a append A tl l2 ].
+  | cons hd tl ⇒  hd a title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/a append A tl l2 ].
 
-definition hd ≝ λA.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.λd:A.
+img class="anchor" src="icons/tick.png" id="hd"definition hd ≝ λA.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.λd:A.
   match l with [ nil ⇒ d | cons a _ ⇒ a].
 
-definition tail ≝  λA.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.
-  match l with [ nil ⇒  [a title="nil" href="cic:/fakeuri.def(1)"]/a | cons hd tl ⇒  tl].
+img class="anchor" src="icons/tick.png" id="tail"definition tail ≝  λA.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.
+  match l with [ nil ⇒  a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a | cons hd tl ⇒  tl].
 
 interpretation "append" 'append l1 l2 = (append ? l1 l2).
 
-theorem append_nil: ∀A.∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.l a title="append" href="cic:/fakeuri.def(1)"@/a [a title="nil" href="cic:/fakeuri.def(1)"]/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
+img class="anchor" src="icons/tick.png" id="append_nil"theorem append_nil: ∀A.∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.l a title="append" href="cic:/fakeuri.def(1)"@/a a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
 #A #l (elim l) normalize // qed.
 
-theorem associative_append: 
+img class="anchor" src="icons/tick.png" id="associative_append"theorem associative_append: 
  ∀A.a href="cic:/matita/basics/relations/associative.def(1)"associative/a (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (a href="cic:/matita/basics/list/append.fix(0,1,1)"append/a A).
 #A #l1 #l2 #l3 (elim l1) normalize // qed.
 
@@ -70,51 +70,51 @@ ntheorem cons_append_commute:
     a :: (l1 @ l2) = (a :: l1) @ l2.
 //; nqed. *)
 
-theorem append_cons:∀A.∀a:A.∀l,l1.la title="append" href="cic:/fakeuri.def(1)"@/a(a:a title="cons" href="cic:/fakeuri.def(1)":/al1)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a(la title="append" href="cic:/fakeuri.def(1)"@/a(a:a title="cons" href="cic:/fakeuri.def(1)":/a[a title="nil" href="cic:/fakeuri.def(1)"]/a))a title="append" href="cic:/fakeuri.def(1)"@/al1.span style="text-decoration: underline;"/spanspan class="autotactic"/span
+img class="anchor" src="icons/tick.png" id="append_cons"theorem append_cons:∀A.∀a:A.∀l,l1.la title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al1)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a(la title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aa title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a))a title="append" href="cic:/fakeuri.def(1)"@/al1.span style="text-decoration: underline;"/spanspan class="autotactic"/span
 #A #a #l1 #l2 >a href="cic:/matita/basics/list/associative_append.def(4)"associative_append/a // qed.
 
-theorem nil_append_elim: ∀A.∀l1,l2: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀P:?→?→Prop. 
-  l1a title="append" href="cic:/fakeuri.def(1)"@/al2a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a[a title="nil" href="cic:/fakeuri.def(1)"]/a → P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) → P l1 l2.
+img class="anchor" src="icons/tick.png" id="nil_append_elim"theorem nil_append_elim: ∀A.∀l1,l2: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀P:?→?→Prop. 
+  l1a title="append" href="cic:/fakeuri.def(1)"@/al2a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a → P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) → P l1 l2.
 #A #l1 #l2 #P (cases l1) normalize //
 #a #l3 #heq destruct
 qed.
 
-theorem nil_to_nil:  ∀A.∀l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.
-  l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a.
+img class="anchor" src="icons/tick.png" id="nil_to_nil"theorem nil_to_nil:  ∀A.∀l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.
+  l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a.
 #A #l1 #l2 #isnil @(a href="cic:/matita/basics/list/nil_append_elim.def(4)"nil_append_elim/a A l1 l2) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/
 qed.
 
 (* iterators *)
 
-let rec map (A,B:Type[0]) (f: A → B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B ≝
- match l with [ nil ⇒ a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a ? | cons x tl ⇒ f x :a title="cons" href="cic:/fakeuri.def(1)":/a (map A B f tl)].
+img class="anchor" src="icons/tick.png" id="map"let rec map (A,B:Type[0]) (f: A → B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B ≝
+ match l with [ nil ⇒ a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a ? | cons x tl ⇒ f x a title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/a (map A B f tl)].
   
-lemma map_append : ∀A,B,f,l1,l2.
+img class="anchor" src="icons/tick.png" id="map_append"lemma map_append : ∀A,B,f,l1,l2.
   (a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f l1) a title="append" href="cic:/fakeuri.def(1)"@/a (a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f l2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f (l1a title="append" href="cic:/fakeuri.def(1)"@/al2).
 #A #B #f #l1 elim l1
 [ #l2 @a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a
 | #h #t #IH #l2 normalize //
 ] qed.
 
-let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l :B ≝  
+img class="anchor" src="icons/tick.png" id="foldr"let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l :B ≝  
  match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
  
-definition filter ≝ 
+img class="anchor" src="icons/tick.png" id="filter"definition filter ≝ 
   λT.λp:T → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a.
-  a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a T (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T) (λx,l0.if (p x) then (x:a title="cons" href="cic:/fakeuri.def(1)":/al0) else l0) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a T).
+  a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a T (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T) (λx,l0.if (p x) then (xa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al0) else l0) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a T).
 
-definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
-    a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a ?? (λi,acc.(a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? (f i) l2)a title="append" href="cic:/fakeuri.def(1)"@/aacc) [ a title="nil" href="cic:/fakeuri.def(1)"]/a l1. 
+img class="anchor" src="icons/tick.png" id="compose"definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
+    a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a ?? (λi,acc.(a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? (f i) l2)a title="append" href="cic:/fakeuri.def(1)"@/aacc) a title="nil" href="cic:/fakeuri.def(1)"[/a a title="nil" href="cic:/fakeuri.def(1)"]/a l1. 
 
-lemma filter_true : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 
-  a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (a:a title="cons" href="cic:/fakeuri.def(1)":/al) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a :a title="cons" href="cic:/fakeuri.def(1)":/a a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l.
+img class="anchor" src="icons/tick.png" id="filter_true"lemma filter_true : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 
+  a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a a title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/a a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l.
 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 
-lemma filter_false : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → 
-  a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (a:a title="cons" href="cic:/fakeuri.def(1)":/al) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l.
+img class="anchor" src="icons/tick.png" id="filter_false"lemma filter_false : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → 
+  a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l.
 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 
-theorem eq_map : ∀A,B,f,g,l. (∀x.f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g x) → a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B g l.
+img class="anchor" src="icons/tick.png" id="eq_map"theorem eq_map : ∀A,B,f,g,l. (∀x.f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g x) → a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B g l.
 #A #B #f #g #l #eqfg (elim l) normalize // qed.
 
 (*
@@ -125,40 +125,40 @@ match l1 with
   ]. *)
 
 (**************************** reverse *****************************)
-let rec rev_append S (l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S) on l1 ≝
+img class="anchor" src="icons/tick.png" id="rev_append"let rec rev_append S (l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S) on l1 ≝
   match l1 with 
   [ nil ⇒ l2
-  | cons a tl ⇒ rev_append S tl (a:a title="cons" href="cic:/fakeuri.def(1)":/al2)
+  | cons a tl ⇒ rev_append S tl (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al2)
   ]
 .
 
-definition reverse ≝λS.λl.a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"rev_append/a S l [a title="nil" href="cic:/fakeuri.def(1)"]/a.
+img class="anchor" src="icons/tick.png" id="reverse"definition reverse ≝λS.λl.a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"rev_append/a S l a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a.
 
-lemma reverse_single : ∀S,a. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (a:a title="cons" href="cic:/fakeuri.def(1)":/a[a title="nil" href="cic:/fakeuri.def(1)"]/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a:a title="cons" href="cic:/fakeuri.def(1)":/a[a title="nil" href="cic:/fakeuri.def(1)"]/a). 
+img class="anchor" src="icons/tick.png" id="reverse_single"lemma reverse_single : ∀S,a. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aa title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aa title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a). 
 // qed.
 
-lemma rev_append_def : ∀S,l1,l2. 
+img class="anchor" src="icons/tick.png" id="rev_append_def"lemma rev_append_def : ∀S,l1,l2. 
   a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"rev_append/a S l1 l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l1) a title="append" href="cic:/fakeuri.def(1)"@/a l2 .
 #S #l1 elim l1 normalize // 
 qed.
 
-lemma reverse_cons : ∀S,a,l. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (a:a title="cons" href="cic:/fakeuri.def(1)":/al) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l)a title="append" href="cic:/fakeuri.def(1)"@/a(a:a title="cons" href="cic:/fakeuri.def(1)":/a[a title="nil" href="cic:/fakeuri.def(1)"]/a).
+img class="anchor" src="icons/tick.png" id="reverse_cons"lemma reverse_cons : ∀S,a,l. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l)a title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aa title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a).
 #S #a #l whd in ⊢ (??%?); // 
 qed.
 
-lemma reverse_append: ∀S,l1,l2. 
+img class="anchor" src="icons/tick.png" id="reverse_append"lemma reverse_append: ∀S,l1,l2. 
   a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (l1 a title="append" href="cic:/fakeuri.def(1)"@/a l2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l2)a title="append" href="cic:/fakeuri.def(1)"@/a(a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l1).
 #S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a
 >a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a // qed.
 
-lemma reverse_reverse : ∀S,l. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
+img class="anchor" src="icons/tick.png" id="reverse_reverse"lemma reverse_reverse : ∀S,l. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
 #S #l elim l // #a #tl #Hind >a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a >a href="cic:/matita/basics/list/reverse_append.def(8)"reverse_append/a 
 normalize // qed.
 
 (* an elimination principle for lists working on the tail;
 useful for strings *)
-lemma list_elim_left: ∀S.∀P:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S → Prop. P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a S) →
-(∀a.∀tl.P tl → P (tla title="append" href="cic:/fakeuri.def(1)"@/a(a:a title="cons" href="cic:/fakeuri.def(1)":/a[a title="nil" href="cic:/fakeuri.def(1)"]/a))) → ∀l. P l.
+img class="anchor" src="icons/tick.png" id="list_elim_left"lemma list_elim_left: ∀S.∀P:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S → Prop. P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a S) →
+(∀a.∀tl.P tl → P (tla title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aa title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a))) → ∀l. P l.
 #S #P #Pnil #Pstep #l <(a href="cic:/matita/basics/list/reverse_reverse.def(9)"reverse_reverse/a … l) 
 generalize in match (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l); #l elim l //
 #a #tl #H >a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a @Pstep //
@@ -166,7 +166,7 @@ qed.
 
 (**************************** length *******************************)
 
-let rec length (A:Type[0]) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l ≝ 
+img class="anchor" src="icons/tick.png" id="length"let rec length (A:Type[0]) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l ≝ 
   match l with 
     [ nil ⇒ a title="natural number" href="cic:/fakeuri.def(1)"0/a
     | cons a tl ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (length A tl)].
@@ -174,19 +174,19 @@ let rec length (A:Type[0]) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"
 notation "|M|" non associative with precedence 60 for @{'norm $M}.
 interpretation "norm" 'norm l = (length ? l).
 
-lemma length_append: ∀A.∀l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A. 
-  |l1a title="append" href="cic:/fakeuri.def(1)"@/al2a title="norm" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l1a title="norm" href="cic:/fakeuri.def(1)"|/aa title="natural plus" href="cic:/fakeuri.def(1)"+/a|l2a title="norm" href="cic:/fakeuri.def(1)"|/a.
+img class="anchor" src="icons/tick.png" id="length_append"lemma length_append: ∀A.∀l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A. 
+  a title="norm" href="cic:/fakeuri.def(1)"|/al1a title="append" href="cic:/fakeuri.def(1)"@/al2a title="norm" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/al1a title="norm" href="cic:/fakeuri.def(1)"|/aa title="natural plus" href="cic:/fakeuri.def(1)"+/aa title="norm" href="cic:/fakeuri.def(1)"|/al2a title="norm" href="cic:/fakeuri.def(1)"|/a.
 #A #l1 elim l1 // normalize /span class="autotactic"2span class="autotrace" trace /span/span/
 qed.
 
-let rec nth n (A:Type[0]) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (d:A)  ≝  
+img class="anchor" src="icons/tick.png" id="nth"let rec nth n (A:Type[0]) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (d:A)  ≝  
   match n with
     [O ⇒ a href="cic:/matita/basics/list/hd.def(1)"hd/a A l d
     |S m ⇒ nth m A (a href="cic:/matita/basics/list/tail.def(1)"tail/a A l) d].
 
 (***************************** fold *******************************)
 
-let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) (f:A→B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l :B ≝  
+img class="anchor" src="icons/tick.png" id="fold"let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) (f:A→B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l :B ≝  
  match l with 
   [ nil ⇒ b 
   | cons a l ⇒ if (p a) then (op (f a) (fold A B op b p f l))
@@ -203,38 +203,38 @@ for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
 
 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
 
-theorem fold_true: 
+img class="anchor" src="icons/tick.png" id="fold_true"theorem fold_true: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 
-  \fold[op,nil]_{i ∈ a:a title="cons" href="cic:/fakeuri.def(1)":/al| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
-    op (f a) \fold[op,nil]_{i ∈ l| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i). 
+  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+    op (f a) a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i). 
 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 
-theorem fold_false: 
+img class="anchor" src="icons/tick.png" id="fold_false"theorem fold_false: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
-p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → \fold[op,nil]_{i ∈ a:a title="cons" href="cic:/fakeuri.def(1)":/al| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
-  \fold[op,nil]_{i ∈ l| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i).
+p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i).
 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 
-theorem fold_filter: 
+img class="anchor" src="icons/tick.png" id="fold_filter"theorem fold_filter: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
-  \fold[op,nil]_{i ∈ l| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
-    \fold[op,nil]_{i ∈ (a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l)a title="\fold" href="cic:/fakeuri.def(1)"}/a (f i).
+  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+    a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ (a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l)a title="\fold" href="cic:/fakeuri.def(1)"}/a (f i).
 #A #B #a #l #p #op #nil #f elim l //  
 #a #tl #Hind cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p a)) #pa 
   [ >a href="cic:/matita/basics/list/filter_true.def(3)"filter_true/a // > a href="cic:/matita/basics/list/fold_true.def(3)"fold_true/a // >a href="cic:/matita/basics/list/fold_true.def(3)"fold_true/a //
   | >a href="cic:/matita/basics/list/filter_false.def(3)"filter_false/a // >a href="cic:/matita/basics/list/fold_false.def(3)"fold_false/a // ]
 qed.
 
-record Aop (A:Type[0]) (nil:A) : Type[0] ≝
+img class="anchor" src="icons/tick.png" id="Aop"record Aop (A:Type[0]) (nil:A) : Type[0] ≝
   {op :2> A → A → A; 
    nill:∀a. op nil a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a; 
    nilr:∀a. op a nil a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a;
    assoc: ∀a,b,c.op a (op b c) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a op (op a b) c
   }.
 
-theorem fold_sum: ∀A,B. ∀I,J:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀nil.∀op:a href="cic:/matita/basics/list/Aop.ind(1,0,2)"Aop/a B nil.∀f.
-  op (\fold[op,nil]_{i∈Ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i)) (\fold[op,nil]_{i∈Ja title="\fold" href="cic:/fakeuri.def(1)"}/a (f i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
-    \fold[op,nil]_{i∈(Ia title="append" href="cic:/fakeuri.def(1)"@/aJ)a title="\fold" href="cic:/fakeuri.def(1)"}/a (f i).
+img class="anchor" src="icons/tick.png" id="fold_sum"theorem fold_sum: ∀A,B. ∀I,J:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀nil.∀op:a href="cic:/matita/basics/list/Aop.ind(1,0,2)"Aop/a B nil.∀f.
+  op (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈Ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i)) (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈Ja title="\fold" href="cic:/fakeuri.def(1)"}/a (f i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
+    a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈(Ia title="append" href="cic:/fakeuri.def(1)"@/aJ)a title="\fold" href="cic:/fakeuri.def(1)"}/a (f i).
 #A #B #I #J #nil #op #f (elim I) normalize 
   [>a href="cic:/matita/basics/list/nill.fix(0,2,2)"nill/a //|#a #tl #Hind <a href="cic:/matita/basics/list/assoc.fix(0,2,2)"assoc/a //]
 qed.
\ No newline at end of file