From adfe42bbd5aaa4130a4133f345930e79444f0f3e Mon Sep 17 00:00:00 2001
From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Wed, 29 May 2013 14:50:41 +0000
Subject: [PATCH] commit by user andrea

---
 weblib/Reverse_complexity/reverse.ma      | 266 +++++++++++-----------
 weblib/arithmetics/bounded_quantifiers.ma |  51 +++++
 weblib/arithmetics/pidgeon_hole.ma        |  90 ++++++++
 weblib/basics/append.ma                   |   1 +
 weblib/basics/list.ma                     |  72 +++---
 weblib/basics/lists/append.ma             |  52 +++++
 weblib/basics/lists/iterators.ma          |  35 +++
 weblib/basics/lists/lists.ma              |  47 ++++
 8 files changed, 444 insertions(+), 170 deletions(-)
 create mode 100644 weblib/arithmetics/bounded_quantifiers.ma
 create mode 100644 weblib/arithmetics/pidgeon_hole.ma
 create mode 100644 weblib/basics/append.ma
 create mode 100644 weblib/basics/lists/append.ma
 create mode 100644 weblib/basics/lists/iterators.ma
 create mode 100644 weblib/basics/lists/lists.ma

diff --git a/weblib/Reverse_complexity/reverse.ma b/weblib/Reverse_complexity/reverse.ma
index 73814b17a..c99de03c5 100644
--- a/weblib/Reverse_complexity/reverse.ma
+++ b/weblib/Reverse_complexity/reverse.ma
@@ -6,11 +6,11 @@ include "arithmetics/bigO.ma".
  
 (*********************************** pairing **********************************) 
 
-axiom pair: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
-axiom fst : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
-axiom snd : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
-axiom fst_pair: ∀a,b. a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a (a href="cic:/matita/Reverse_complexity/reverse/pair.dec"pair/a a b) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a.
-axiom snd_pair: ∀a,b. a href="cic:/matita/Reverse_complexity/reverse/snd.dec"snd/a (a href="cic:/matita/Reverse_complexity/reverse/pair.dec"pair/a a b) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b. 
+img class="anchor" src="icons/tick.png" id="pair"axiom pair: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+img class="anchor" src="icons/tick.png" id="fst"axiom fst : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+img class="anchor" src="icons/tick.png" id="snd"axiom snd : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+img class="anchor" src="icons/tick.png" id="fst_pair"axiom fst_pair: ∀a,b. a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a (a href="cic:/matita/Reverse_complexity/reverse/pair.dec"pair/a a b) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a.
+img class="anchor" src="icons/tick.png" id="snd_pair"axiom snd_pair: ∀a,b. a href="cic:/matita/Reverse_complexity/reverse/snd.dec"snd/a (a href="cic:/matita/Reverse_complexity/reverse/pair.dec"pair/a a b) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b. 
 
 interpretation "abstract pair" 'pair f g = (pair f g).
 
@@ -19,10 +19,10 @@ interpretation "abstract pair" 'pair f g = (pair f g).
 (* u is the deterministic configuration relation of the universal machine (one 
    step) *)
 
-axiom u: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/basics/types/option.ind(1,0,1)"option/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+img class="anchor" src="icons/tick.png" id="u"axiom u: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/basics/types/option.ind(1,0,1)"option/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
 
-let rec U c n on n ≝ 
-  match n with  
+img class="anchor" src="icons/tick.png" id="U"let rec U c n on n ≝ 
+  match n in nat with  
   [ O ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ?
   | S m ⇒ match a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a c with 
     [ None ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? c (* halting case *)
@@ -30,12 +30,12 @@ let rec U c n on n ≝
     ]
   ].
  
-lemma halt_U: ∀i,n,y. a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a i.
+img class="anchor" src="icons/tick.png" id="halt_U"lemma halt_U: ∀i,n,y. a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a i.
 #i #n #y #H cases n
   [normalize #H1 destruct |#m normalize >H normalize #H1 destruct //]
 qed. 
 
-lemma Some_to_halt: ∀n,i,y. a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? .
+img class="anchor" src="icons/tick.png" id="Some_to_halt"lemma Some_to_halt: ∀n,i,y. a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? .
 #n elim n
   [#i #y normalize #H destruct (H)
   |#m #Hind #i #y normalize 
@@ -45,7 +45,7 @@ lemma Some_to_halt: ∀n,i,y. a href="cic:/matita/Reverse_complexity/reverse/U.
   ]
 qed. 
 
-lemma monotonici_U: ∀y,n,m,i.
+img class="anchor" src="icons/tick.png" id="monotonici_U"lemma monotonici_U: ∀y,n,m,i.
   a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i (na title="natural plus" href="cic:/fakeuri.def(1)"+/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y.
 #y #n #m elim m 
   [#i normalize #H destruct 
@@ -56,7 +56,7 @@ lemma monotonici_U: ∀y,n,m,i.
   ]
 qed.
 
-lemma monotonic_U: ∀i,n,m,y.n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/am →
+img class="anchor" src="icons/tick.png" id="monotonic_U"lemma monotonic_U: ∀i,n,m,y.n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/am →
   a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y.
 #i #n #m #y #lenm #H >(a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a m n) // @a href="cic:/matita/Reverse_complexity/reverse/monotonici_U.def(5)"monotonici_U/a //
 qed.
@@ -65,7 +65,7 @@ qed.
 (* axiom monotonic_U: ∀i,n,m,y.n ≤m →
    U i n = Some ? y → U i m = Some ? y. *)
   
-lemma unique_U: ∀i,n,m,yn,ym.
+img class="anchor" src="icons/tick.png" id="unique_U"lemma unique_U: ∀i,n,m,yn,ym.
   a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? yn → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? ym → yn a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ym.
 #i #n #m #yn #ym #Hn #Hm cases (a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"decidable_le/a n m)
   [#lenm lapply (a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"monotonic_U/a … lenm Hn) >Hm #HS destruct (HS) //
@@ -74,16 +74,16 @@ lemma unique_U: ∀i,n,m,yn,ym.
   ]
 qed.
 
-definition code_for ≝ λf,i.∀x.
+img class="anchor" src="icons/tick.png" id="code_for"definition code_for ≝ λf,i.∀x.
   a title="exists" href="cic:/fakeuri.def(1)"∃/an.∀m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈i,xa title="abstract pair" href="cic:/fakeuri.def(1)"〉/a m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f x.
 
-definition terminate ≝ λc,r. a title="exists" href="cic:/fakeuri.def(1)"∃/ay. a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a c r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y.
+img class="anchor" src="icons/tick.png" id="terminate"definition terminate ≝ λc,r. a title="exists" href="cic:/fakeuri.def(1)"∃/ay. a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a c r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y.
 
 interpretation "termination" 'fintersects c r = (terminate c r).
  
-definition lang ≝ λi,x.a title="exists" href="cic:/fakeuri.def(1)"∃/ar,ya title="exists" href="cic:/fakeuri.def(1)"./a a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈i,xa title="abstract pair" href="cic:/fakeuri.def(1)"〉/a r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y a title="logical and" href="cic:/fakeuri.def(1)"∧/a a title="natural number" href="cic:/fakeuri.def(1)"0/a  a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a y. 
+img class="anchor" src="icons/tick.png" id="lang"definition lang ≝ λi,x.a title="exists" href="cic:/fakeuri.def(1)"∃/ar,ya title="exists" href="cic:/fakeuri.def(1)"./a a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈i,xa title="abstract pair" href="cic:/fakeuri.def(1)"〉/a r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y a title="logical and" href="cic:/fakeuri.def(1)"∧/a a title="natural number" href="cic:/fakeuri.def(1)"0/a  a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a y. 
 
-lemma lang_cf :∀f,i,x. a href="cic:/matita/Reverse_complexity/reverse/code_for.def(2)"code_for/a f i → 
+img class="anchor" src="icons/tick.png" id="lang_cf"lemma lang_cf :∀f,i,x. a href="cic:/matita/Reverse_complexity/reverse/code_for.def(2)"code_for/a f i → 
   a href="cic:/matita/Reverse_complexity/reverse/lang.def(2)"lang/a i x a title="iff" href="cic:/fakeuri.def(1)"↔/a a title="exists" href="cic:/fakeuri.def(1)"∃/ay.f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y a title="logical and" href="cic:/fakeuri.def(1)"∧/a a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a y.
 #f #i #x normalize #H %
   [* #n * #y * #H1 #posy %{y} % // 
@@ -95,175 +95,173 @@ qed.
 
 (******************************* complexity classes ***************************)
 
-axiom size: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
-axiom of_size: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+img class="anchor" src="icons/tick.png" id="size"axiom size: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+img class="anchor" src="icons/tick.png" id="of_size"axiom of_size: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
 
 interpretation "size" 'card n = (size n).
 
-axiom size_of_size: ∀n. |a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a na title="size" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n.
-axiom of_size_max: ∀i,n. |ia title="size" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a n.
+img class="anchor" src="icons/tick.png" id="size_of_size"axiom size_of_size: ∀n. |a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a na title="size" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n.
+img class="anchor" src="icons/tick.png" id="of_size_max"axiom of_size_max: ∀i,n. |ia title="size" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a n.
 
-axiom size_fst : ∀n. |a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a na title="size" href="cic:/fakeuri.def(1)"|/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a |na title="size" href="cic:/fakeuri.def(1)"|/a.
+img class="anchor" src="icons/tick.png" id="size_fst"axiom size_fst : ∀n. |a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a na title="size" href="cic:/fakeuri.def(1)"|/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a |na title="size" href="cic:/fakeuri.def(1)"|/a.
 
-axiom a : Max0.
+img class="anchor" src="icons/tick.png" id="size_f"definition size_f ≝ λf,n.Max_{ifont class="Apple-style-span" color="#FF0000" < /fonta href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a n) | a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a (|ia title="size" href="cic:/fakeuri.def(1)"|/a) n a title="bigop" href="cic:/fakeuri.def(1)"}/a|(f i)a title="size" href="cic:/fakeuri.def(1)"|/a.
 
-definition size_f ≝ λf,n.Max_{ifont class="Apple-style-span" color="#FF0000" < /fontS (of_size n) | eqb (|i|) n }|(f i)|.
-
-lemma size_f_def: ∀f,n. size_f f n = 
-  Max_{i < S (of_size n) | eqb (|i|) n}|(f i)|.
+img class="anchor" src="icons/tick.png" id="size_f_def"lemma size_f_def: ∀f,n. a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a f n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+  Max_{i < a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a n) | a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a (|ia title="size" href="cic:/fakeuri.def(1)"|/a) na title="bigop" href="cic:/fakeuri.def(1)"}/a|(f i)a title="size" href="cic:/fakeuri.def(1)"|/a.
 // qed.
 
-lemma size_f_size : ∀f,n. size_f (f ∘ size) n = |(f n)|.
-#f #n @le_to_le_to_eq
-  [@Max_le #a #lta #Ha normalize >(eqb_true_to_eq  … Ha) //
-  |<(size_of_size n) in ⊢ (?%?); >size_f_def
-   @(le_Max (λi.|f (|i|)|) ? (S (of_size n)) (of_size n) ??)
-    [@le_S_S // | @eq_to_eqb_true //]
+img class="anchor" src="icons/tick.png" id="size_f_size"lemma size_f_size : ∀f,n. a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a (f a title="function composition" href="cic:/fakeuri.def(1)"∘/a a href="cic:/matita/Reverse_complexity/reverse/size.dec"size/a) n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |(f n)a title="size" href="cic:/fakeuri.def(1)"|/a.
+#f #n @a href="cic:/matita/arithmetics/nat/le_to_le_to_eq.def(5)"le_to_le_to_eq/a
+  [@a href="cic:/matita/arithmetics/min_max/Max_le.def(9)"Max_le/a #a #lta #Ha normalize >(a href="cic:/matita/arithmetics/nat/eqb_true_to_eq.def(6)"eqb_true_to_eq/a  … Ha) //
+  |<(a href="cic:/matita/Reverse_complexity/reverse/size_of_size.dec"size_of_size/a n) in ⊢ (?%?); >a href="cic:/matita/Reverse_complexity/reverse/size_f_def.def(4)"size_f_def/a
+   @(a href="cic:/matita/arithmetics/min_max/le_Max.def(12)"le_Max/a (λi.|f (|ia title="size" href="cic:/fakeuri.def(1)"|/a)a title="size" href="cic:/fakeuri.def(1)"|/a) ? (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a n)) (a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a n) ??)
+    [@a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a // | @a href="cic:/matita/arithmetics/nat/eq_to_eqb_true.def(5)"eq_to_eqb_true/a //]
   ]
 qed.
 
-lemma size_f_id : ∀n. size_f (λx.x) n = n.
-#n @le_to_le_to_eq
-  [@Max_le #a #lta #Ha >(eqb_true_to_eq  … Ha) //
-  |<(size_of_size n) in ⊢ (?%?); >size_f_def
-   @(le_Max (λi.|i|) ? (S (of_size n)) (of_size n) ??)
-    [@le_S_S // | @eq_to_eqb_true //]
+img class="anchor" src="icons/tick.png" id="size_f_id"lemma size_f_id : ∀n. a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a (λx.x) n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n.
+#n @a href="cic:/matita/arithmetics/nat/le_to_le_to_eq.def(5)"le_to_le_to_eq/a
+  [@a href="cic:/matita/arithmetics/min_max/Max_le.def(9)"Max_le/a #a #lta #Ha >(a href="cic:/matita/arithmetics/nat/eqb_true_to_eq.def(6)"eqb_true_to_eq/a  … Ha) //
+  |<(a href="cic:/matita/Reverse_complexity/reverse/size_of_size.dec"size_of_size/a n) in ⊢ (?%?); >a href="cic:/matita/Reverse_complexity/reverse/size_f_def.def(4)"size_f_def/a
+   @(a href="cic:/matita/arithmetics/min_max/le_Max.def(12)"le_Max/a (λi.|ia title="size" href="cic:/fakeuri.def(1)"|/a) ? (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a n)) (a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a n) ??)
+    [@a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a // | @a href="cic:/matita/arithmetics/nat/eq_to_eqb_true.def(5)"eq_to_eqb_true/a //]
   ]
 qed.
 
-lemma size_f_fst : ∀n. size_f fst n ≤ n.
-#n @Max_le #a #lta #Ha <(eqb_true_to_eq  … Ha) //
+img class="anchor" src="icons/tick.png" id="size_f_fst"lemma size_f_fst : ∀n. a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
+#n @a href="cic:/matita/arithmetics/min_max/Max_le.def(9)"Max_le/a #a #lta #Ha <(a href="cic:/matita/arithmetics/nat/eqb_true_to_eq.def(6)"eqb_true_to_eq/a  … Ha) //
 qed.
 
 (* definition def ≝ λf:nat → option nat.λx.∃y. f x = Some ? y.*)
 
 (* C s i means that the complexity of i is O(s) *)
 
-definition C ≝ λs,i.∃c.∃a.∀x.a ≤ |x| → ∃y. 
-  U 〈i,x〉 (c*(s(|x|))) = Some ? y.
+img class="anchor" src="icons/tick.png" id="C"definition C ≝ λs,i.a title="exists" href="cic:/fakeuri.def(1)"∃/ac.a title="exists" href="cic:/fakeuri.def(1)"∃/aa.∀x.a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a |xa title="size" href="cic:/fakeuri.def(1)"|/a → a title="exists" href="cic:/fakeuri.def(1)"∃/ay. 
+  a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈i,xa title="abstract pair" href="cic:/fakeuri.def(1)"〉/a (ca title="natural times" href="cic:/fakeuri.def(1)"*/a(s(|xa title="size" href="cic:/fakeuri.def(1)"|/a))) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y.
 
-definition CF ≝ λs,f.∃i.code_for f i ∧ C s i.
+img class="anchor" src="icons/tick.png" id="CF"definition CF ≝ λs,f.a title="exists" href="cic:/fakeuri.def(1)"∃/ai.a href="cic:/matita/Reverse_complexity/reverse/code_for.def(2)"code_for/a f i a title="logical and" href="cic:/fakeuri.def(1)"∧/a a href="cic:/matita/Reverse_complexity/reverse/C.def(3)"C/a s i.
 
-lemma ext_CF : ∀f,g,s. (∀n. f n = g n) → CF s f → CF s g.
+img class="anchor" src="icons/tick.png" id="ext_CF"lemma ext_CF : ∀f,g,s. (∀n. f n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g n) → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s f → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s g.
 #f #g #s #Hext * #i * #Hcode #HC %{i} %
   [#x cases (Hcode x) #a #H %{a} <Hext @H | //] 
 qed. 
 
-lemma monotonic_CF: ∀s1,s2,f. O s2 s1 → CF s1 f → CF s2 f.
+img class="anchor" src="icons/tick.png" id="monotonic_CF"lemma monotonic_CF: ∀s1,s2,f. a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s2 s1 → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s1 f → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s2 f.
 #s1 #s2 #f * #c1 * #a #H * #i * #Hcodef #HCs1 %{i} % //
-cases HCs1 #c2 * #b #H2 %{(c2*c1)} %{(max a b)} 
-#x #Hmax cases (H2 x ?) [2:@(le_maxr … Hmax)] #y #Hy
-%{y} @(monotonic_U …Hy) >associative_times @le_times // @H @(le_maxl … Hmax)
+cases HCs1 #c2 * #b #H2 %{(c2a title="natural times" href="cic:/fakeuri.def(1)"*/ac1)} %{(a href="cic:/matita/arithmetics/nat/max.def(2)"max/a a b)} 
+#x #Hmax cases (H2 x ?) [2:@(a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"le_maxr/a … Hmax)] #y #Hy
+%{y} @(a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"monotonic_U/a …Hy) >a href="cic:/matita/arithmetics/nat/associative_times.def(10)"associative_times/a @a href="cic:/matita/arithmetics/nat/le_times.def(9)"le_times/a // @H @(a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"le_maxl/a … Hmax)
 qed. 
 
 (************************** The diagonal language *****************************)
 
 (* the diagonal language used for the hierarchy theorem *)
 
-definition diag ≝ λs,i. 
-  U 〈fst i,i〉 (s (|i|)) = Some ? 0. 
+img class="anchor" src="icons/tick.png" id="diag"definition diag ≝ λs,i. 
+  a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a i,ia title="abstract pair" href="cic:/fakeuri.def(1)"〉/a (s (|ia title="size" href="cic:/fakeuri.def(1)"|/a)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? a title="natural number" href="cic:/fakeuri.def(1)"0/a. 
 
-lemma equiv_diag: ∀s,i. 
-  diag s i ↔ 〈fst i, i〉 ↓ s (|i|) ∧ ¬lang (fst i) i.
+img class="anchor" src="icons/tick.png" id="equiv_diag"lemma equiv_diag: ∀s,i. 
+  a href="cic:/matita/Reverse_complexity/reverse/diag.def(2)"diag/a s i a title="iff" href="cic:/fakeuri.def(1)"↔/a 〈a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a i, ia title="abstract pair" href="cic:/fakeuri.def(1)"〉/a a title="termination" href="cic:/fakeuri.def(1)"↓/a s (|ia title="size" href="cic:/fakeuri.def(1)"|/a) a title="logical and" href="cic:/fakeuri.def(1)"∧/a a title="logical not" href="cic:/fakeuri.def(1)"¬/aa href="cic:/matita/Reverse_complexity/reverse/lang.def(2)"lang/a (a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a i) i.
 #s #i %
-  [whd in ⊢ (%→?); #H % [%{0} //] % * #x * #y *
-   #H1 #Hy cut (0 = y) [@(unique_U … H H1)] #eqy /2/
+  [whd in ⊢ (%→?); #H % [%{a title="natural number" href="cic:/fakeuri.def(1)"0/a} //] % * #x * #y *
+   #H1 #Hy cut (a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y) [@(a href="cic:/matita/Reverse_complexity/reverse/unique_U.def(9)"unique_U/a … H H1)] #eqy /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
   |* * #y cases y //
-   #y0 #H * #H1 @False_ind @H1 -H1 whd %{(s (|i|))} %{(S y0)} % //
+   #y0 #H * #H1 @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @H1 -H1 whd %{(s (|ia title="size" href="cic:/fakeuri.def(1)"|/a))} %{(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a y0)} % //
   ]
 qed.
 
 (* Let us define the characteristic function diag_cf for diag, and prove
 it correctness *)
 
-definition diag_cf ≝ λs,i.
-  match U 〈fst i,i〉 (s (|i|)) with
-  [ None ⇒ None ?
-  | Some y ⇒ if (eqb y 0) then (Some ? 1) else (Some ? 0)].
+img class="anchor" src="icons/tick.png" id="diag_cf"definition diag_cf ≝ λs,i.
+  match a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a i,ia title="abstract pair" href="cic:/fakeuri.def(1)"〉/a (s (|ia title="size" href="cic:/fakeuri.def(1)"|/a)) with
+  [ None ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ?
+  | Some y ⇒ if (a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a y a title="natural number" href="cic:/fakeuri.def(1)"0/a) then (a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? a title="natural number" href="cic:/fakeuri.def(1)"1/a) else (a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? a title="natural number" href="cic:/fakeuri.def(1)"0/a)].
 
-lemma diag_cf_OK: ∀s,x. diag s x ↔ ∃y.diag_cf s x = Some ? y ∧ 0 < y.
+img class="anchor" src="icons/tick.png" id="diag_cf_OK"lemma diag_cf_OK: ∀s,x. a href="cic:/matita/Reverse_complexity/reverse/diag.def(2)"diag/a s x a title="iff" href="cic:/fakeuri.def(1)"↔/a a title="exists" href="cic:/fakeuri.def(1)"∃/ay.a href="cic:/matita/Reverse_complexity/reverse/diag_cf.def(2)"diag_cf/a s x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y a title="logical and" href="cic:/fakeuri.def(1)"∧/a a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a y.
 #s #x % 
-  [whd in ⊢ (%→?); #H %{1} % // whd in ⊢ (??%?); >H // 
+  [whd in ⊢ (%→?); #H %{a title="natural number" href="cic:/fakeuri.def(1)"1/a} % // whd in ⊢ (??%?); >H // 
   |* #y * whd in ⊢ (??%?→?→%); 
-   cases (U 〈fst x,x〉 (s (|x|))) normalize
+   cases (a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a x,xa title="abstract pair" href="cic:/fakeuri.def(1)"〉/a (s (|xa title="size" href="cic:/fakeuri.def(1)"|/a))) normalize
     [#H destruct
-    |#x cases (true_or_false (eqb x 0)) #Hx >Hx 
-      [>(eqb_true_to_eq … Hx) // 
-      |normalize #H destruct #H @False_ind @(absurd ? H) @lt_to_not_le //  
+    |#x cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a x a title="natural number" href="cic:/fakeuri.def(1)"0/a)) #Hx >Hx 
+      [>(a href="cic:/matita/arithmetics/nat/eqb_true_to_eq.def(6)"eqb_true_to_eq/a … Hx) // 
+      |normalize #H destruct #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a ? H) @a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a //  
       ]
     ]
   ]
 qed.
 
-lemma diag_spec: ∀s,i. code_for (diag_cf s) i → ∀x. lang i x ↔ diag s x.
-#s #i #Hcode #x @(iff_trans  … (lang_cf … Hcode)) @iff_sym @diag_cf_OK
+img class="anchor" src="icons/tick.png" id="diag_spec"lemma diag_spec: ∀s,i. a href="cic:/matita/Reverse_complexity/reverse/code_for.def(2)"code_for/a (a href="cic:/matita/Reverse_complexity/reverse/diag_cf.def(2)"diag_cf/a s) i → ∀x. a href="cic:/matita/Reverse_complexity/reverse/lang.def(2)"lang/a i x a title="iff" href="cic:/fakeuri.def(1)"↔/a a href="cic:/matita/Reverse_complexity/reverse/diag.def(2)"diag/a s x.
+#s #i #Hcode #x @(a href="cic:/matita/basics/logic/iff_trans.def(2)"iff_trans/a  … (a href="cic:/matita/Reverse_complexity/reverse/lang_cf.def(10)"lang_cf/a … Hcode)) @a href="cic:/matita/basics/logic/iff_sym.def(2)"iff_sym/a @a href="cic:/matita/Reverse_complexity/reverse/diag_cf_OK.def(8)"diag_cf_OK/a
 qed. 
 
 (******************************************************************************)
 
-lemma absurd1: ∀P. iff P (¬ P) →False.
-#P * #H1 #H2 cut (¬P) [% #H2 @(absurd … H2) @H1 //] 
-#H3 @(absurd ?? H3) @H2 @H3 
+img class="anchor" src="icons/tick.png" id="absurd1"lemma absurd1: ∀P. a href="cic:/matita/basics/logic/iff.def(1)"iff/a P (a title="logical not" href="cic:/fakeuri.def(1)"¬/a P) →a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a.
+#P * #H1 #H2 cut (a title="logical not" href="cic:/fakeuri.def(1)"¬/aP) [% #H2 @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … H2) @H1 //] 
+#H3 @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a ?? H3) @H2 @H3 
 qed.
 
 (* axiom weak_pad : ∀a,∃a0.∀n. a0 < n → ∃b. |〈a,b〉| = n. *)
-axiom pad : ∀a,n. |a| < n → ∃b. |〈a,b〉| = n.
+img class="anchor" src="icons/tick.png" id="pad"axiom pad : ∀a,n. |aa title="size" href="cic:/fakeuri.def(1)"|/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a title="exists" href="cic:/fakeuri.def(1)"∃/ab. |〈a,ba title="abstract pair" href="cic:/fakeuri.def(1)"〉/aa title="size" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n.
 
-lemma not_included_ex: ∀s1,s2. not_O s2 s1 → ∀i. C s2 i →
-  ∃b.〈i, 〈i,b〉〉 ↓ s1 (|〈i,b〉|).
+img class="anchor" src="icons/tick.png" id="not_included_ex"lemma not_included_ex: ∀s1,s2. a href="cic:/matita/arithmetics/bigO/not_O.def(3)"not_O/a s2 s1 → ∀i. a href="cic:/matita/Reverse_complexity/reverse/C.def(3)"C/a s2 i →
+  a title="exists" href="cic:/fakeuri.def(1)"∃/ab.〈i, 〈i,ba title="abstract pair" href="cic:/fakeuri.def(1)"〉/aa title="abstract pair" href="cic:/fakeuri.def(1)"〉/a a title="termination" href="cic:/fakeuri.def(1)"↓/a s1 (|〈i,ba title="abstract pair" href="cic:/fakeuri.def(1)"〉/aa title="size" href="cic:/fakeuri.def(1)"|/a).
 #s1 #s2  #H #i * #c * #x0 #H1 
-cases (H c (max (S(|i|)) x0)) #x1 * #H2 #H3 cases (pad i x1 ?) 
+cases (H c (a href="cic:/matita/arithmetics/nat/max.def(2)"max/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(|ia title="size" href="cic:/fakeuri.def(1)"|/a)) x0)) #x1 * #H2 #H3 cases (a href="cic:/matita/Reverse_complexity/reverse/pad.dec"pad/a i x1 ?) 
   [#b #H4 %{b}
-   cases (H1 〈i,b〉 ?)
-    [#z >H4 #H5 %{z} @(monotonic_U … H5) @lt_to_le //
-    |>H4 @(le_maxr … H2)
+   cases (H1 〈i,ba title="abstract pair" href="cic:/fakeuri.def(1)"〉/a ?)
+    [#z >H4 #H5 %{z} @(a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"monotonic_U/a … H5) @a href="cic:/matita/arithmetics/nat/lt_to_le.def(6)"lt_to_le/a //
+    |>H4 @(a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"le_maxr/a … H2)
     ]
-  |@(le_maxl … H2)
+  |@(a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"le_maxl/a … H2)
   ]
 qed.
 
-lemma diag1_not_s1: ∀s1,s2. not_O s2 s1 → ¬ CF s2 (diag_cf s1).
+img class="anchor" src="icons/tick.png" id="diag1_not_s1"lemma diag1_not_s1: ∀s1,s2. a href="cic:/matita/arithmetics/bigO/not_O.def(3)"not_O/a s2 s1 → a title="logical not" href="cic:/fakeuri.def(1)"¬/a a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s2 (a href="cic:/matita/Reverse_complexity/reverse/diag_cf.def(2)"diag_cf/a s1).
 #s1 #s2 #H1 % * #i * #Hcode_i #Hs2_i 
-cases (not_included_ex  … H1 ? Hs2_i) #b #H2
-lapply (diag_spec … Hcode_i) #H3
-@(absurd1 (lang i 〈i,b〉))
-@(iff_trans … (H3 〈i,b〉)) 
-@(iff_trans … (equiv_diag …)) >fst_pair 
+cases (a href="cic:/matita/Reverse_complexity/reverse/not_included_ex.def(10)"not_included_ex/a  … H1 ? Hs2_i) #b #H2
+lapply (a href="cic:/matita/Reverse_complexity/reverse/diag_spec.def(11)"diag_spec/a … Hcode_i) #H3
+@(a href="cic:/matita/Reverse_complexity/reverse/absurd1.def(3)"absurd1/a (a href="cic:/matita/Reverse_complexity/reverse/lang.def(2)"lang/a i 〈i,ba title="abstract pair" href="cic:/fakeuri.def(1)"〉/a))
+@(a href="cic:/matita/basics/logic/iff_trans.def(2)"iff_trans/a … (H3 〈i,ba title="abstract pair" href="cic:/fakeuri.def(1)"〉/a)) 
+@(a href="cic:/matita/basics/logic/iff_trans.def(2)"iff_trans/a … (a href="cic:/matita/Reverse_complexity/reverse/equiv_diag.def(10)"equiv_diag/a …)) >a href="cic:/matita/Reverse_complexity/reverse/fst_pair.dec"fst_pair/a 
 %[* #_ // |#H6 % // ]
 qed.
 
 (******************************************************************************)
 (* definition sumF ≝ λf,g:nat→nat.λn.f n + g n. *)
 
-definition to_Some ≝ λf.λx:nat. Some nat (f x).
+img class="anchor" src="icons/tick.png" id="to_Some"definition to_Some ≝ λf.λx:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a (f x).
 
-definition deopt ≝ λn. match n with 
-  [ None ⇒ 1
+img class="anchor" src="icons/tick.png" id="deopt"definition deopt ≝ λn. match n with 
+  [ None ⇒ a title="natural number" href="cic:/fakeuri.def(1)"1/a
   | Some n ⇒ n].
   
-definition opt_comp ≝ λf,g:nat → option nat. λx.
+img class="anchor" src="icons/tick.png" id="opt_comp"definition opt_comp ≝ λf,g:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/basics/types/option.ind(1,0,1)"option/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. λx.
   match g x with 
-  [ None ⇒ None ?
+  [ None ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ?
   | Some y ⇒ f y ].   
 
 (* axiom CFU: ∀h,g,s. CF s (to_Some h)  → CF s (to_Some (of_size ∘ g)) → 
   CF (Slow s) (λx.U (h x) (g x)). *)
   
-axiom sU2: nat → nat → nat.
-axiom sU: nat → nat → nat → nat.
+img class="anchor" src="icons/tick.png" id="sU2"axiom sU2: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+img class="anchor" src="icons/tick.png" id="sU"axiom sU: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
 
 (* axiom CFU: CF sU (λx.U (fst x) (snd x)). *)
 
-axiom CFU: ∀h,g,f,s1,s2,s3. 
-  CF s1 (to_Some h)  → CF s2 (to_Some g) → CF s3 (to_Some f) → 
-  CF (λx. s1 x + s2 x + s3 x + sU (size_f h x) (size_f g x) (size_f f x)) 
-    (λx.U 〈h x,g x〉 (|f x|)).
+img class="anchor" src="icons/tick.png" id="CFU"axiom CFU: ∀h,g,f,s1,s2,s3. 
+  a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s1 (a href="cic:/matita/Reverse_complexity/reverse/to_Some.def(1)"to_Some/a h)  → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s2 (a href="cic:/matita/Reverse_complexity/reverse/to_Some.def(1)"to_Some/a g) → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s3 (a href="cic:/matita/Reverse_complexity/reverse/to_Some.def(1)"to_Some/a f) → 
+  a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a (λx. s1 x a title="natural plus" href="cic:/fakeuri.def(1)"+/a s2 x a title="natural plus" href="cic:/fakeuri.def(1)"+/a s3 x a title="natural plus" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/Reverse_complexity/reverse/sU.dec"sU/a (a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a h x) (a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a g x) (a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a f x)) 
+    (λx.a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈h x,g xa title="abstract pair" href="cic:/fakeuri.def(1)"〉/a (|f xa title="size" href="cic:/fakeuri.def(1)"|/a)).
     
-axiom monotonic_sU: ∀a1,a2,b1,b2,c1,c2. a1 ≤ a2 → b1 ≤ b2 → c1 ≤c2 →
-  sU a1 b1 c1 ≤ sU a2 b2 c2.
+img class="anchor" src="icons/tick.png" id="monotonic_sU"axiom monotonic_sU: ∀a1,a2,b1,b2,c1,c2. a1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a2 → b1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b2 → c1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/ac2 →
+  a href="cic:/matita/Reverse_complexity/reverse/sU.dec"sU/a a1 b1 c1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/Reverse_complexity/reverse/sU.dec"sU/a a2 b2 c2.
 
-definition sU_space ≝ λi,x,r.i+x+r.
-definition sU_time ≝ λi,x,r.i+x+(i^2)*r*(log 2 r).
+(* definition sU_space ≝ λi,x,r.i+x+r.
+definition sU_time ≝ λi,x,r.i+x+(i^2)*r*(log 2 r). *)
 
 (*
 axiom CF_comp: ∀f,g,s1, s2. CF s1 f → CF s2 g → 
@@ -275,33 +273,33 @@ axiom CF_comp: ∀f,g,s1, s2. CF s1 f → CF s2 g →
 axiom CF_comp_strong: ∀f,g,s1,s2. CF s1 f → CF s2 g → 
   CF (s1 ∘ s2) (opt_comp f g). *)
 
-definition IF ≝ λb,f,g:nat →option nat. λx.
+img class="anchor" src="icons/tick.png" id="IF"definition IF ≝ λb,f,g:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a →a href="cic:/matita/basics/types/option.ind(1,0,1)"option/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. λx.
   match b x with 
-  [None ⇒ None ?
-  |Some n ⇒ if (eqb n 0) then f x else g x].
+  [None ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ?
+  |Some n ⇒ if (a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a n a title="natural number" href="cic:/fakeuri.def(1)"0/a) then f x else g x].
 
-axiom IF_CF: ∀b,f,g,sb,sf,sg. CF sb b → CF sf f → CF sg g → 
-  CF (λn. sb n + sf n + sg n) (IF b f g).
+img class="anchor" src="icons/tick.png" id="IF_CF"axiom IF_CF: ∀b,f,g,sb,sf,sg. a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a sb b → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a sf f → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a sg g → 
+  a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a (λn. sb n a title="natural plus" href="cic:/fakeuri.def(1)"+/a sf n a title="natural plus" href="cic:/fakeuri.def(1)"+/a sg n) (a href="cic:/matita/Reverse_complexity/reverse/IF.def(2)"IF/a b f g).
 
-lemma diag_cf_def : ∀s.∀i. 
-  diag_cf s i =  
-    IF (λi.U (pair (fst i) i) (|of_size (s (|i|))|)) (λi.Some ? 1) (λi.Some ? 0) i.
-#s #i normalize >size_of_size // qed. 
+img class="anchor" src="icons/tick.png" id="diag_cf_def"lemma diag_cf_def : ∀s.∀i. 
+  a href="cic:/matita/Reverse_complexity/reverse/diag_cf.def(2)"diag_cf/a s i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a  
+    a href="cic:/matita/Reverse_complexity/reverse/IF.def(2)"IF/a (λi.a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a (a href="cic:/matita/Reverse_complexity/reverse/pair.dec"pair/a (a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a i) i) (|a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a (s (|ia title="size" href="cic:/fakeuri.def(1)"|/a))a title="size" href="cic:/fakeuri.def(1)"|/a)) (λi.a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? a title="natural number" href="cic:/fakeuri.def(1)"1/a) (λi.a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? a title="natural number" href="cic:/fakeuri.def(1)"0/a) i.
+#s #i normalize >a href="cic:/matita/Reverse_complexity/reverse/size_of_size.dec"size_of_size/a // qed. 
 
 (* and now ... *)
-axiom CF_pair: ∀f,g,s. CF s (λx.Some ? (f x)) → CF s (λx.Some ? (g x)) → 
-  CF s (λx.Some ? (pair (f x) (g x))).
+img class="anchor" src="icons/tick.png" id="CF_pair"axiom CF_pair: ∀f,g,s. a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s (λx.a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (f x)) → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s (λx.a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (g x)) → 
+  a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s (λx.a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (a href="cic:/matita/Reverse_complexity/reverse/pair.dec"pair/a (f x) (g x))).
 
-axiom CF_fst: ∀f,s. CF s (λx.Some ? (f x)) → CF s (λx.Some ? (fst (f x))).
+img class="anchor" src="icons/tick.png" id="CF_fst"axiom CF_fst: ∀f,s. a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s (λx.a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (f x)) → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s (λx.a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a (f x))).
 
-definition minimal ≝ λs. CF s (λn. Some ? n) ∧ ∀c. CF s (λn. Some ? c).
+img class="anchor" src="icons/tick.png" id="minimal"definition minimal ≝ λs. a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s (λn. a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? n) a title="logical and" href="cic:/fakeuri.def(1)"∧/a ∀c. a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s (λn. a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? c).
 
 
 (*
 axiom le_snd: ∀n. |snd n| ≤ |n|.
 axiom daemon: ∀P:Prop.P. *)
 
-definition constructible ≝ λs. CF s (λx.Some ? (of_size (s (|x|)))).
+img class="anchor" src="icons/tick.png" id="constructible"definition constructible ≝ λs. a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s (λx.a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a (s (|xa title="size" href="cic:/fakeuri.def(1)"|/a)))).
 
 (*
 lemma compl1: ∀s. 
@@ -318,20 +316,20 @@ lemma compl1: ∀s.
 #s #H1 #H2 #H3 @monotonic_CF [3: @(CFU ??? s s s) @CFU //
 qed.  *)
 
-lemma diag_s: ∀s. minimal s → constructible s → 
-  CF (λx.s x + sU x x (s x)) (diag_cf s).
+img class="anchor" src="icons/tick.png" id="diag_s"lemma diag_s: ∀s. a href="cic:/matita/Reverse_complexity/reverse/minimal.def(5)"minimal/a s → a href="cic:/matita/Reverse_complexity/reverse/constructible.def(5)"constructible/a s → 
+  a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a (λx.s x a title="natural plus" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/Reverse_complexity/reverse/sU.dec"sU/a x x (s x)) (a href="cic:/matita/Reverse_complexity/reverse/diag_cf.def(2)"diag_cf/a s).
 #s * #Hs_id #Hs_c #Hs_constr 
-@ext_CF [2: #n @sym_eq @diag_cf_def | skip]
-@(monotonic_CF ???? (IF_CF (λi:ℕ.U (pair (fst i) i) (|of_size (s (|i|))|))
-   … (λi.s i + s i + s i + (sU (size_f fst i) (size_f (λi.i) i) (size_f (λi.of_size (s (|i|))) i))) … (Hs_c 1) (Hs_c 0) … ))
-  [2: @CFU [@CF_fst // | // |@Hs_constr]
-  |@(O_ext2 (λn:ℕ.s n+sU (size_f fst n) n (s n) + (s n+s n+s n+s n))) 
-    [2: #i >size_f_size >size_of_size >size_f_id //] 
-   @O_absorbr 
-    [%{1} %{0} #n #_ >commutative_times <times_n_1 @le_plus //
-     @monotonic_sU // 
-    |@O_plus_l @(O_plus … (O_refl s)) @(O_plus … (O_refl s)) 
-     @(O_plus … (O_refl s)) //
+@a href="cic:/matita/Reverse_complexity/reverse/ext_CF.def(5)"ext_CF/a [2: #n @a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a @a href="cic:/matita/Reverse_complexity/reverse/diag_cf_def.def(3)"diag_cf_def/a | skip]
+@(a href="cic:/matita/Reverse_complexity/reverse/monotonic_CF.def(11)"monotonic_CF/a ???? (a href="cic:/matita/Reverse_complexity/reverse/IF_CF.dec"IF_CF/a (λi:a title="Natural numbers" href="cic:/fakeuri.def(1)"ℕ/a.a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a (a href="cic:/matita/Reverse_complexity/reverse/pair.dec"pair/a (a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a i) i) (|a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a (s (|ia title="size" href="cic:/fakeuri.def(1)"|/a))a title="size" href="cic:/fakeuri.def(1)"|/a))
+   … (λi.s i a title="natural plus" href="cic:/fakeuri.def(1)"+/a s i a title="natural plus" href="cic:/fakeuri.def(1)"+/a s i a title="natural plus" href="cic:/fakeuri.def(1)"+/a (a href="cic:/matita/Reverse_complexity/reverse/sU.dec"sU/a (a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a i) (a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a (λi.i) i) (a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a (λi.a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a (s (|ia title="size" href="cic:/fakeuri.def(1)"|/a))) i))) … (Hs_c a title="natural number" href="cic:/fakeuri.def(1)"1/a) (Hs_c a title="natural number" href="cic:/fakeuri.def(1)"0/a) … ))
+  [2: @a href="cic:/matita/Reverse_complexity/reverse/CFU.dec"CFU/a [@a href="cic:/matita/Reverse_complexity/reverse/CF_fst.dec"CF_fst/a // | // |@Hs_constr]
+  |@(a href="cic:/matita/arithmetics/bigO/O_ext2.def(4)"O_ext2/a (λn:a title="Natural numbers" href="cic:/fakeuri.def(1)"ℕ/a.s na title="natural plus" href="cic:/fakeuri.def(1)"+/aa href="cic:/matita/Reverse_complexity/reverse/sU.dec"sU/a (a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a n) n (s n) a title="natural plus" href="cic:/fakeuri.def(1)"+/a (s na title="natural plus" href="cic:/fakeuri.def(1)"+/as na title="natural plus" href="cic:/fakeuri.def(1)"+/as na title="natural plus" href="cic:/fakeuri.def(1)"+/as n))) 
+    [2: #i >a href="cic:/matita/Reverse_complexity/reverse/size_f_size.def(13)"size_f_size/a >a href="cic:/matita/Reverse_complexity/reverse/size_of_size.dec"size_of_size/a >a href="cic:/matita/Reverse_complexity/reverse/size_f_id.def(13)"size_f_id/a //] 
+   @a href="cic:/matita/arithmetics/bigO/O_absorbr.def(12)"O_absorbr/a 
+    [%{a title="natural number" href="cic:/fakeuri.def(1)"1/a} %{a title="natural number" href="cic:/fakeuri.def(1)"0/a} #n #_ >a href="cic:/matita/arithmetics/nat/commutative_times.def(8)"commutative_times/a <a href="cic:/matita/arithmetics/nat/times_n_1.def(8)"times_n_1/a @a href="cic:/matita/arithmetics/nat/le_plus.def(7)"le_plus/a //
+     @a href="cic:/matita/Reverse_complexity/reverse/monotonic_sU.dec"monotonic_sU/a // 
+    |@a href="cic:/matita/arithmetics/bigO/O_plus_l.def(10)"O_plus_l/a @(a href="cic:/matita/arithmetics/bigO/O_plus.def(10)"O_plus/a … (a href="cic:/matita/arithmetics/bigO/O_refl.def(9)"O_refl/a s)) @(a href="cic:/matita/arithmetics/bigO/O_plus.def(10)"O_plus/a … (a href="cic:/matita/arithmetics/bigO/O_refl.def(9)"O_refl/a s)) 
+     @(a href="cic:/matita/arithmetics/bigO/O_plus.def(10)"O_plus/a … (a href="cic:/matita/arithmetics/bigO/O_refl.def(9)"O_refl/a s)) //
   ]
 qed.
 
@@ -348,12 +346,12 @@ theorem hierarchy_theorem_right: ∀s1,s2:nat→nat.
 qed.
 *)
 
-theorem hierarchy_theorem_left: ∀s1,s2:nat→nat.
-   O(s1) ⊆ O(s2) → CF s1 ⊆ CF s2.
+img class="anchor" src="icons/tick.png" id="hierarchy_theorem_left"theorem hierarchy_theorem_left: ∀s1,s2:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+   a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a(s1) a title="subset" href="cic:/fakeuri.def(1)"⊆/a a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a(s2) → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s1 a title="subset" href="cic:/fakeuri.def(1)"⊆/a a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s2.
 #s1 #s2 #HO #f * #i * #Hcode * #c * #a #Hs1_i %{i} % //
-cases (sub_O_to_O … HO) -HO #c1 * #b #Hs1s2 
-%{(c*c1)} %{(max a b)} #x #lemax 
-cases (Hs1_i x ?) [2: @(le_maxl …lemax)]
-#y #Hy %{y} @(monotonic_U … Hy) >associative_times
-@le_times // @Hs1s2 @(le_maxr … lemax)
+cases (a href="cic:/matita/arithmetics/bigO/sub_O_to_O.def(10)"sub_O_to_O/a … HO) -HO #c1 * #b #Hs1s2 
+%{(ca title="natural times" href="cic:/fakeuri.def(1)"*/ac1)} %{(a href="cic:/matita/arithmetics/nat/max.def(2)"max/a a b)} #x #lemax 
+cases (Hs1_i x ?) [2: @(a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"le_maxl/a …lemax)]
+#y #Hy %{y} @(a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"monotonic_U/a … Hy) >a href="cic:/matita/arithmetics/nat/associative_times.def(10)"associative_times/a
+@a href="cic:/matita/arithmetics/nat/le_times.def(9)"le_times/a // @Hs1s2 @(a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"le_maxr/a … lemax)
 qed.
\ No newline at end of file
diff --git a/weblib/arithmetics/bounded_quantifiers.ma b/weblib/arithmetics/bounded_quantifiers.ma
new file mode 100644
index 000000000..6eef112e3
--- /dev/null
+++ b/weblib/arithmetics/bounded_quantifiers.ma
@@ -0,0 +1,51 @@
+include "arithmetics/nat.ma".
+
+img class="anchor" src="icons/tick.png" id="decidable_not"lemma decidable_not: ∀P. a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a P → a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (a title="logical not" href="cic:/fakeuri.def(1)"¬/aP).
+#P * #H [%2 % * /span class="autotactic"2span class="autotrace" trace /span/span/ | /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/] 
+qed.
+
+img class="anchor" src="icons/tick.png" id="decidable_or"lemma decidable_or: ∀P,Q. a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a P → a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a Q → a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (Pa title="logical or" href="cic:/fakeuri.def(1)"∨/aQ).
+#P #Q * #HP [#_ %1 %1 // |* #HQ [ %1 %2 // | %2 % * /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/] 
+qed.
+
+img class="anchor" src="icons/tick.png" id="decidable_forall"lemma decidable_forall: ∀P. (∀i.a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (P i))→ 
+  ∀n.a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (∀i. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → P i).
+#P #Hdec #n elim n
+  [%1 #i #lti0 @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … lti0) @a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"le_to_not_lt/a //
+  |#m * #H
+    [cases (Hdec m) #HPm
+      [%1 #i #lei0 cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … lei0) #H1
+        [@H @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @H1 |>(a href="cic:/matita/arithmetics/nat/injective_S.def(4)"injective_S/a … H1) @HPm]
+      |%2 @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … HPm) #H1 @H1 //
+      ]
+    |%2 @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … H) #H1 #i #leim @H1 @a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a //
+    ]
+  ]
+qed.
+
+img class="anchor" src="icons/tick.png" id="not_exists_to_forall"lemma not_exists_to_forall: ∀P,n.
+  a title="logical not" href="cic:/fakeuri.def(1)"¬/a(a title="exists" href="cic:/fakeuri.def(1)"∃/ai. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="logical and" href="cic:/fakeuri.def(1)"∧/a P i) → ∀i. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a title="logical not" href="cic:/fakeuri.def(1)"¬/a P i.
+#P #n elim n 
+  [#_ #i #lti0 @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … lti0) @a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"le_to_not_lt/a //
+  |#m #Hind #H1 #i #leiS cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … leiS) #H2
+    [@(Hind … (a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a … H2)) @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … H1) *
+     #a * #leam #Pa %{a} % // @a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a //
+    |@(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … H1) #Pi %{i} % //
+    ]
+  ]
+qed. 
+ 
+img class="anchor" src="icons/tick.png" id="not_forall_to_exists"lemma not_forall_to_exists: ∀P,n. (∀i.a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (P i)) → 
+  a title="logical not" href="cic:/fakeuri.def(1)"¬/a(∀i. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → P i) → (a title="exists" href="cic:/fakeuri.def(1)"∃/ai. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="logical and" href="cic:/fakeuri.def(1)"∧/a a title="logical not" href="cic:/fakeuri.def(1)"¬/a (P i)).
+#P #n #decP elim n
+  [* #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @H #i #lti0 @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … lti0) @a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"le_to_not_lt/a //
+  |#m #Hind #H1 cases (decP m) #H2
+    [cases (Hind ?)
+      [#i * #leim #nPi %{i} % // @a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a //
+      |@(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … H1) #H3 #i #leiS cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … leiS)
+        [#ltiS @H3 @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a // |#eqi //]
+      ]
+    |%{m} % //
+    ]
+  ]
+qed.
\ No newline at end of file
diff --git a/weblib/arithmetics/pidgeon_hole.ma b/weblib/arithmetics/pidgeon_hole.ma
new file mode 100644
index 000000000..e4aed1629
--- /dev/null
+++ b/weblib/arithmetics/pidgeon_hole.ma
@@ -0,0 +1,90 @@
+
+include "arithmetics/bounded_quantifiers.ma".
+include "basics/list.ma".
+
+(* A bit of combinatorics *)
+interpretation "list membership" 'mem a l = (mem ? a l).
+
+lemma decidable_mem_nat: ∀n:nat.∀l. decidable (n ∈ l).
+#n #l elim l
+  [%2 % @False_ind |#a #tl #Htl @decidable_or //]
+qed.
+
+lemma length_unique_le: ∀n,l. unique ? l  → (∀x. x ∈ l → x < n) → |l| ≤ n.
+#n elim n 
+  [* // #a #tl #_ #H @False_ind @(absurd (a < 0)) 
+    [@H %1 % | @le_to_not_lt //]
+  |#m #Hind #l #Huni #Hmem <(filter_length2 ? (eqb m) l)
+   lapply (length_filter_eqb … m l Huni) #Hle
+   @(transitive_le ? (1+|filter ? (λx.¬ eqb m x) l|))
+    [@le_plus // 
+    |@le_S_S @Hind
+      [@unique_filter // 
+      |#x #memx cut (x ≤ m)
+        [@le_S_S_to_le @Hmem @(mem_filter … memx)] #Hcut
+       cases(le_to_or_lt_eq … Hcut) // #eqxm @False_ind
+       @(absurd ? eqxm) @sym_not_eq @eqb_false_to_not_eq
+       @injective_notb @(mem_filter_true ???? memx)
+      ]
+    ]
+  ]
+qed.    
+
+lemma eq_length_to_mem : ∀n,l. |l| = S n → unique ? l → 
+  (∀x. x ∈ l → x ≤ n) → n ∈ l.
+#n #l #H1 #H2 #H3 cases (decidable_mem_nat n l) // 
+#H4 @False_ind @(absurd (|l| > n))
+  [>H1 // 
+  |@le_to_not_lt @length_unique_le //
+   #x #memx cases(le_to_or_lt_eq … (H3 x memx)) //
+   #Heq @not_le_to_lt @(not_to_not … H4) #_ <Heq //
+  ]
+qed.
+
+lemma eq_length_to_mem_all: ∀n,l. |l| = n → unique ? l  → 
+  (∀x. x ∈ l → x < n) → ∀i. i < n → i ∈ l.
+#n elim n
+  [#l #_ #_ #_ #i #lti0 @False_ind @(absurd ? lti0 (not_le_Sn_O ?))
+  |#m #Hind #l #H #H1 #H2 #i #lei cases (le_to_or_lt_eq … lei)
+    [#leim @(mem_filter… (λi.¬(eqb m i))) 
+     cases (filter_eqb m … H1)
+      [2: * #H @False_ind @(absurd ?? H) @eq_length_to_mem //
+       #x #memx @le_S_S_to_le @H2 //]
+      * #memm #Hfilter @Hind
+        [@injective_S <H <(filter_length2 ? (eqb m) l) >Hfilter %
+        |@unique_filter @H1
+        |#x #memx cases (le_to_or_lt_eq … (H2 x (mem_filter … memx))) #H3
+          [@le_S_S_to_le @H3
+          |@False_ind @(absurd (m=x)) [@injective_S //] @eqb_false_to_not_eq
+           @injective_notb >(mem_filter_true ???? memx) %
+          ]
+      |@le_S_S_to_le @leim
+      ]
+    |#eqi @eq_length_to_mem >eqi [@H |@H1 |#x #Hx @le_S_S_to_le >eqi @H2 //]
+    ]
+  ]
+qed. 
+
+lemma lt_length_to_not_mem: ∀n,l. unique ? l  → (∀x. x ∈ l → x < n) → |l| < n →
+∃i. i < n ∧ ¬ (i ∈ l). 
+#n elim n
+  [#l #_ #_ #H @False_ind /2/
+  |#m #Hind #l #Huni #Hmem #Hlen cases (filter_eqb m … Huni)
+    [2: * #H #_ %{m} % //
+    |* #memm #Hfilter cases (Hind (filter ? (λx. ¬(eqb m x)) l) ? ? ?)
+      [#i * #ltim #memi %{i} % [@le_S // ]
+       @(not_to_not … memi) @mem_filter_l @injective_notb >notb_notb
+       @not_eq_to_eqb_false @sym_not_eq @lt_to_not_eq //
+      |@unique_filter //
+      |#x #memx cases (le_to_or_lt_eq … (Hmem x ?))
+        [#H @le_S_S_to_le @H
+        |#H @False_ind @(absurd (m=x)) [@injective_S //] @eqb_false_to_not_eq
+         @injective_notb >(mem_filter_true ???? memx) %
+        |@(mem_filter … memx)
+        ]
+      |<(filter_length2 … (eqb m)) in Hlen; >Hfilter #H
+       @le_S_S_to_le @H
+      ]
+    ]
+  ]
+qed.
\ No newline at end of file
diff --git a/weblib/basics/append.ma b/weblib/basics/append.ma
new file mode 100644
index 000000000..5fe5dcee7
--- /dev/null
+++ b/weblib/basics/append.ma
@@ -0,0 +1 @@
+(* new script *)
\ No newline at end of file
diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma
index d542416c4..49cc0a5af 100644
--- a/weblib/basics/list.ma
+++ b/weblib/basics/list.ma
@@ -11,7 +11,7 @@
 
 include "arithmetics/nat.ma".
 
-img class="anchor" src="icons/tick.png" id="list"inductive list (A:Type[0]) : Type[0] :=
+inductive list (A:Type[0]) : Type[0] :=
   | nil: list A
   | cons: A -> list A -> list A.
 
@@ -30,10 +30,10 @@ notation "hvbox(l1 break @ l2)"
 interpretation "nil" 'nil = (nil ?).
 interpretation "cons" 'cons hd tl = (cons ? hd tl).
 
-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 ≝
+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 ].
 
-img class="anchor" src="icons/tick.png" id="nil_cons"theorem 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 ]. *)
 
-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 ≝ 
+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)":/aa title="cons" href="cic:/fakeuri.def(1)":/a append A tl l2 ].
 
-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.
+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].
 
-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.
+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).
 
-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.
+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.
 
-img class="anchor" src="icons/tick.png" id="associative_append"theorem 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. *)
 
-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
+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.
 
-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. 
+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.
 
-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.
+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 *)
 
-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 ≝
+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)].
   
-img class="anchor" src="icons/tick.png" id="map_append"lemma map_append : ∀A,B,f,l1,l2.
+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.
 
-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 ≝  
+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)].
  
-img class="anchor" src="icons/tick.png" id="filter"definition 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 (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).
 
-img class="anchor" src="icons/tick.png" id="compose"definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
+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. 
 
-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 → 
+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.
 
-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 → 
+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.
 
-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.
+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,39 +125,39 @@ match l1 with
   ]. *)
 
 (**************************** reverse *****************************)
-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 ≝
+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 (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al2)
   ]
 .
 
-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.
+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.
 
-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). 
+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.
 
-img class="anchor" src="icons/tick.png" id="rev_append_def"lemma rev_append_def : ∀S,l1,l2. 
+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.
 
-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).
+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.
 
-img class="anchor" src="icons/tick.png" id="reverse_append"lemma reverse_append: ∀S,l1,l2. 
+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.
 
-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.
+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 *)
-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) →
+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 //
@@ -166,7 +166,7 @@ qed.
 
 (**************************** length *******************************)
 
-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 ≝ 
+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 @@ qed.
 notation "|M|" non associative with precedence 60 for @{'norm $M}.
 interpretation "norm" 'norm l = (length ? l).
 
-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. 
+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.
 
-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)  ≝  
+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 *******************************)
 
-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 ≝  
+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,19 +203,19 @@ 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).
 
-img class="anchor" src="icons/tick.png" id="fold_true"theorem 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 → 
   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.
 
-img class="anchor" src="icons/tick.png" id="fold_false"theorem 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 → 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.
 
-img class="anchor" src="icons/tick.png" id="fold_filter"theorem fold_filter: 
+theorem fold_filter: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
   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).
@@ -225,14 +225,14 @@ p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic
   | >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.
 
-img class="anchor" src="icons/tick.png" id="Aop"record Aop (A:Type[0]) (nil:A) : Type[0] ≝
+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
   }.
 
-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.
+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 
diff --git a/weblib/basics/lists/append.ma b/weblib/basics/lists/append.ma
new file mode 100644
index 000000000..73fbd36cc
--- /dev/null
+++ b/weblib/basics/lists/append.ma
@@ -0,0 +1,52 @@
+(* append *)
+
+include "basics/lists/lists.ma".
+include "basics/relations.ma".
+
+img class="anchor" src="icons/tick.png" id="append"let rec append A (l1: a href="cic:/matita/basics/lists/lists/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 ].
+
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
+
+img class="anchor" src="icons/tick.png" id="append_nil"theorem append_nil: ∀A.∀l:a href="cic:/matita/basics/lists/lists/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.
+#A #l (elim l) normalize // qed.
+
+img class="anchor" src="icons/tick.png" id="associative_append"theorem associative_append: 
+ ∀A.font class="Apple-style-span" color="#FF0000"a href="cic:/matita/basics/relations/associative.def(1)"associative/a /font(a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) (a href="cic:/matita/basics/lists/append/append.fix(0,1,1)"append/a A).
+#A #l1 #l2 #l3 (elim l1) normalize // qed.
+
+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(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)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aaa title="nil" href="cic:/fakeuri.def(1)"]/a)a title="append" href="cic:/fakeuri.def(1)"@/al1.
+#A #a #l #l1 >a href="cic:/matita/basics/lists/append/associative_append.def(4)"associative_append/a // qed.
+
+img class="anchor" src="icons/tick.png" id="nil_append_elim"theorem nil_append_elim: ∀A.∀l1,l2: a href="cic:/matita/basics/lists/lists/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/lists/lists/list.con(0,1,1)"nil/a A) (a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"nil/a A) → P l1 l2.
+#A #l1 #l2 #P (cases l1) normalize //
+#a #l3 #heq destruct
+qed.
+
+img class="anchor" src="icons/tick.png" id="nil_to_nil"theorem nil_to_nil:  ∀A.∀l1,l2:a href="cic:/matita/basics/lists/lists/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.
+#A #l1 #l2 #isnil @(a href="cic:/matita/basics/lists/append/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.
+
+(* comparing lists *)
+
+img class="anchor" src="icons/tick.png" id="compare_append"lemma compare_append : ∀A,l1,l2,l3,l4. l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l3a title="append" href="cic:/fakeuri.def(1)"@/al4 → 
+∃l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a Aa title="exists" href="cic:/fakeuri.def(1)"./a(l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l3a title="append" href="cic:/fakeuri.def(1)"@/al a title="logical and" href="cic:/fakeuri.def(1)"∧/a l4a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ala title="append" href="cic:/fakeuri.def(1)"@/al2) a title="logical or" href="cic:/fakeuri.def(1)"∨/a (l3 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l1a title="append" href="cic:/fakeuri.def(1)"@/al a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ala title="append" href="cic:/fakeuri.def(1)"@/al4).
+#A #l1 elim l1
+  [#l2 #l3 #l4 #Heq %{l3} %2 % // @Heq
+  |#a1 #tl1 #Hind #l2 #l3 cases l3
+    [#l4 #Heq %{(a1:a title="cons" href="cic:/fakeuri.def(1)":/atl1)} %1 % // @a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a @Heq 
+    |#a3 #tl3 #l4 normalize in ⊢ (%→?); #Heq cases (Hind l2 tl3 l4 ?)
+      [#l * * #Heq1 #Heq2 %{l}
+        [%1 % // >Heq1 >(a href="cic:/matita/basics/lists/lists/cons_injective_l.def(4)"cons_injective_l/a ????? Heq) //
+        |%2 % // >Heq1 >(a href="cic:/matita/basics/lists/lists/cons_injective_l.def(4)"cons_injective_l/a ????? Heq) //
+        ]
+      |@(a href="cic:/matita/basics/lists/lists/cons_injective_r.def(4)"cons_injective_r/a ????? Heq) 
+      ]
+    ]
+  ]
+qed.
+
diff --git a/weblib/basics/lists/iterators.ma b/weblib/basics/lists/iterators.ma
new file mode 100644
index 000000000..d4497a18b
--- /dev/null
+++ b/weblib/basics/lists/iterators.ma
@@ -0,0 +1,35 @@
+(**************************** iterators ******************************)
+
+include "basics/lists/append.ma".
+
+let rec map (A,B:Type[0]) (f: A span class="error" title="Parse error: RPAREN expected after [term] (in [arg])"→/span B) (l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) on l: a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a B ≝
+ match l with [ nil ⇒ a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"nil/a ? | cons x tl ⇒ f x font class="Apple-style-span" color="#FF0000":/fonta title="cons" href="cic:/fakeuri.def(1)":/a (map A B f tl)].
+
+lemma map_append : ∀A,B,f,l1,l2.
+  (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
+#A #B #f #l1 elim l1 [ #l2 @refl | #h #t #IH #l2 normalize //] 
+qed.
+  
+let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝  
+ match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
+ 
+definition filter ≝ 
+  λT.λp:T → bool.
+  foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T).
+
+(* compose f [a1;...;an] [b1;...;bm] = 
+  [f a1 b1; ... ;f an b1; ... ;f a1 bm; f an bm] *)
+ 
+definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
+    foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1.
+
+lemma filter_true : ∀A,l,a,p. p a = true → 
+  filter A p (a::l) = a :: filter A p l.
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
+
+lemma filter_false : ∀A,l,a,p. p a = false → 
+  filter A p (a::l) = filter 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 = g x) → map A B f l = map A B g l.
+#A #B #f #g #l #eqfg (elim l) normalize // qed.
\ No newline at end of file
diff --git a/weblib/basics/lists/lists.ma b/weblib/basics/lists/lists.ma
new file mode 100644
index 000000000..ba7e48477
--- /dev/null
+++ b/weblib/basics/lists/lists.ma
@@ -0,0 +1,47 @@
+(* Definition of list *)
+
+include "basics/logic.ma".
+
+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.
+
+notation "hvbox(hd break :: tl)"
+  right associative with precedence 47
+  for @{'cons $hd $tl}.
+
+notation "[ list0 term 19 x sep ; ]"
+  non associative with precedence 90
+  for ${fold right @'nil rec acc @{'cons $x $acc}}.
+
+notation "hvbox(l1 break @ l2)"
+  right associative with precedence 47
+  for @{'append $l1 $l2 }.
+
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
+
+img class="anchor" src="icons/tick.png" id="is_nil"definition is_nil: ∀A:Type[0].a href="cic:/matita/basics/lists/lists/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 ].
+
+img class="anchor" src="icons/tick.png" id="nil_cons"theorem nil_cons:
+  ∀A:Type[0].∀l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.∀a:A. a:a 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/lists/lists/is_nil.def(1)"is_nil/a ? (a:a title="cons" href="cic:/fakeuri.def(1)":/al))) >Heq //
+qed.
+
+(* hd and tail *)
+img class="anchor" src="icons/tick.png" id="hd"definition hd ≝ λA.λl: a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.λd:A.
+  match l with [ nil ⇒ d | cons a _ ⇒ a].
+
+img class="anchor" src="icons/tick.png" id="tail"definition tail ≝  λA.λl: a href="cic:/matita/basics/lists/lists/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].
+
+(* injectivity *) 
+
+img class="anchor" src="icons/tick.png" id="cons_injective_l"lemma cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.a1:a title="cons" href="cic:/fakeuri.def(1)":/al1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a2:a title="cons" href="cic:/fakeuri.def(1)":/al2 → a1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a2.
+#A #a1 #a2 #l1 #l2 #Heq destruct //
+qed.
+
+img class="anchor" src="icons/tick.png" id="cons_injective_r"lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1:a title="cons" href="cic:/fakeuri.def(1)":/al1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a2:a title="cons" href="cic:/fakeuri.def(1)":/al2 → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l2.
+#A #a1 #a2 #l1 #l2 #Heq destruct //
+qed.
-- 
2.39.2