From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Fri, 2 Mar 2012 15:25:37 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~1915
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=7956b9a84e0556d2d24fffedbbbabcd9e248d702

commit by user andrea
---

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index ab758c124..11eb476e0 100644
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -171,12 +171,12 @@ We first write down the function, and then discuss it.*)
 
 let rec div2 n ≝ 
 match n with
-[ O ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a,a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉
+[ O ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/aspan class="error" title="Parse error: [sym,] expected after [term level 19] (in [term])"/span,a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉
 | S a ⇒ span style="text-decoration: underline;"/span
    let p ≝ (div2 a) in
-   match (a href="cic:/matita/basics/types/snd.def(1)"snd/a … p) with
-   [ tt ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/basics/types/fst.def(1)"fst/a … p),a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉 
-   | ff ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … p, a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉
+   match (a href="cic:/matita/basics/types/snd.fix(0,2,1)"snd/aspan class="error" title="Parse error: SYMBOL ':' or RPAREN expected after [term] (in [term])"/span … p) with
+   [ tt ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/basics/types/fst.fix(0,2,1)"fst/a … p),a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉 
+   | ff ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.fix(0,2,1)"fst/a … p, a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉
    ]
 ]. 
 
@@ -202,21 +202,21 @@ the remainder for a). The reader is strongly invited to check all remaining deta
 Let us now prove that our div2 function has the expected behaviour.
 *)
 
-lemma surjective_pairing: ∀A,B.∀p:Aa title="Product" href="cic:/fakeuri.def(1)"×/aB. p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … p,a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a … p〉.
+lemma surjective_pairing: ∀A,B.∀p:Aa title="Product" href="cic:/fakeuri.def(1)"×/aB. p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.fix(0,2,1)"fst/a … p,a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/aspan class="error" title="Parse error: [sym〉] or [sym,] expected after [term level 19] (in [term])"/span … p〉.
 #A #B * // qed.
 
 lemma div2SO: ∀n,q. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉 → a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a n) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aspan style="text-decoration: underline;"/spanq,a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉.
 #n #q #H normalize >H normalize // qed.
 
-lemma div2S1: ∀n,q. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉 → a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a n) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a q,a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉.
+lemma div2S1: ∀n,q. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉 → a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a n) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aspan class="error" title="Parse error: [term] expected after [sym=] (in [term])"/span a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a q,a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉.
 #n #q #H normalize >H normalize // qed.
 
 lemma div2_ok: ∀n,q,r. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,r〉 → n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a q) (a href="cic:/matita/tutorial/chapter2/nat_of_bool.def(1)"nat_of_bool/a r).
 #n elim n
   [#q #r normalize #H destruct //
   |#a #Hind #q #r 
-   cut (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a), a href="cic:/matita/basics/types/snd.def(1)"snd/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a)〉) [//] 
-   cases (a href="cic:/matita/basics/types/snd.def(1)"snd/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a))
+   cut (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.fix(0,2,1)"fst/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a), a href="cic:/matita/basics/types/snd.fix(0,2,1)"snd/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a)〉) [//] 
+   cases (a href="cic:/matita/basics/types/snd.fix(0,2,1)"snd/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a))
     [#H >(a href="cic:/matita/tutorial/chapter2/div2S1.def(3)"div2S1/a … H) #H1 destruct @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a span style="text-decoration: underline;">/spana href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a whd in ⊢ (???%); <a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @(Hind … H) 
     |#H >(a href="cic:/matita/tutorial/chapter2/div2SO.def(3)"div2SO/a … H) #H1 destruct >a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a @(Hind … H) 
     ]
@@ -248,7 +248,7 @@ definition qr_spec ≝ λn.λp.∀q,r. p a title="leibnitz's equality" href="ci
 (* We can now construct a function from n to {p|qr_spec n p} by composing the objects
 we already have *)
 
-definition div2P: ∀n.a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,2)" Sub/a (a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"nat/aa title="Product" href="cic:/fakeuri.def(1)"×/aspan style="text-decoration: underline;"a href="cic:/matita/tutorial/chapter2/bool.ind(1,0,0)"bool/a/span) (a href="cic:/matita/tutorial/chapter2/qr_spec.def(3)"qr_spec/a n) ≝ λn.
+definition div2P: ∀n. a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,2)"Sub/a (a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"nat/aa title="Product" href="cic:/fakeuri.def(1)"×/aspan style="text-decoration: underline;"a href="cic:/matita/tutorial/chapter2/bool.ind(1,0,0)"bool/a/span) (a href="cic:/matita/tutorial/chapter2/qr_spec.def(3)"qr_spec/a n) ≝ λn.
  a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a ?? (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n) (a href="cic:/matita/tutorial/chapter2/div2_ok.def(4)"div2_ok/a n).
 
 (* But we can also try do directly build such an object *)
@@ -257,11 +257,11 @@ definition div2Pagain : ∀n.a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,
 #n elim n
   [@(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a,a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉) normalize #q #r #H destruct //
   |#a * #p #qrspec 
-   cut (p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … p, a href="cic:/matita/basics/types/snd.def(1)"snd/a … p〉) [//] 
-   cases (a href="cic:/matita/basics/types/snd.def(1)"snd/a … p)
-    [#H @(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/basics/types/fst.def(1)"fst/a … p),a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉) whd #q #r #H1 destruct @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a span style="text-decoration: underline;">/spana href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a
+   cut (p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.fix(0,2,1)"fst/a … p, a href="cic:/matita/basics/types/snd.fix(0,2,1)"snd/a … p〉) [//] 
+   cases (a href="cic:/matita/basics/types/snd.fix(0,2,1)"snd/a … p)
+    [#H @(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/basics/types/fst.fix(0,2,1)"fst/a … p),a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉) whd #q #r #H1 destruct @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a span style="text-decoration: underline;">/spana href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a
      whd in ⊢ (???%); <a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @(qrspec … H)
-    |#H @(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … p,a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉) whd #q #r #H1 destruct >a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a @(qrspec … H) 
+    |#H @(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.fix(0,2,1)"fst/a … p,a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉) whd #q #r #H1 destruct >a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a @(qrspec … H) 
   ]
 qed.
 
diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma
index f7ad91557..3d7eb7a56 100644
--- a/weblib/tutorial/chapter3.ma
+++ b/weblib/tutorial/chapter3.ma
@@ -59,14 +59,14 @@ function.*)
 let rec append A (l1: a href="cic:/matita/tutorial/chapter3/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)":/aspan class="error" title="Parse error: [sym:] expected after [sym:] (in [term])"/span: append A tl l2 ].
 
 interpretation "append" 'append l1 l2 = (append ? l1 l2).
 
 (* As usual, the function is executable. For instance, (append A nil l) reduces to
 l, as shown by the following example: *)
 
-example nil_append: ∀A.∀l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A. a title="nil" href="cic:/fakeuri.def(1)"[/a] a title="append" href="cic:/fakeuri.def(1)"@/a l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
+example nil_append: ∀A.∀l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A. a title="nil" href="cic:/fakeuri.def(1)"[/aspan class="error" title="Parse error: [term] expected after [sym[] (in [term])"/span] a title="append" href="cic:/fakeuri.def(1)"@/a l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
 #A #l normalize // qed.
 
 (* Proving that l @ [] = l is just a bit more complex. The situation is exactly 
@@ -74,7 +74,7 @@ the same as for the addition operation of the previous chapter: since append is
 defined by recutsion over the first argument, the computation of l @ [] is stuck, 
 and we must proceed by induction on l *) 
 
-lemma append_nil: ∀A.∀l:a href="cic:/matita/tutorial/chapter3/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.
+lemma append_nil: ∀A.∀l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A.l a title="append" href="cic:/fakeuri.def(1)"@/aspan class="error" title="Parse error: [term level 46] expected after [sym@] (in [term])"/spanspan class="error" title="Parse error: [term level 46] expected after [sym@] (in [term])"/span 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.
 
 (* similarly, we can define the two functions head and tail. Since we can only define
@@ -88,7 +88,7 @@ definition head ≝ λA.λl: a href="cic:/matita/tutorial/chapter3/list.ind(1,0
 definition tail ≝  λA.λl: a href="cic:/matita/tutorial/chapter3/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].
 
-example ex_head: ∀A.∀a,d,l. a href="cic:/matita/tutorial/chapter3/head.def(1)"head/a A (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) d a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a.
+example ex_head: ∀A.∀a,d,l. a href="cic:/matita/tutorial/chapter3/head.def(1)"head/a A (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) d a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aspan class="error" title="Parse error: [term] expected after [sym=] (in [term])"/spanspan class="error" title="Parse error: [term] expected after [sym=] (in [term])"/span a.
 #A #a #d #l normalize // qed.
 
 (* Problemi con la notazione *)
@@ -123,7 +123,7 @@ let rec nth n (A:Type[0]) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0
 example ex_length: a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"length/a ? (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="nil" href="cic:/fakeuri.def(1)"[/a]) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a.
 normalize // qed.
 
-example ex_nth: a href="cic:/matita/tutorial/chapter3/nth.fix(0,0,2)"nth/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a) ? (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a) (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="nil" href="cic:/fakeuri.def(1)"[/a])) a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a.
+example ex_nth: a href="cic:/matita/tutorial/chapter3/nth.fix(0,0,2)"nth/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a) ? (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a) (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="nil" href="cic:/fakeuri.def(1)"[/aspan class="error" title="Parse error: [term] expected after [sym[] (in [term])"/span])) a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a.
 normalize // qed.
 
 (* Proving that the length of l1@l2 is the sum of the lengths of l1
@@ -196,7 +196,7 @@ otherwise. We use an if_then_else function included from bool.ma to this purpose
 
 definition filter ≝ 
   λT.λp:T → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a.
-  a href="cic:/matita/tutorial/chapter3/foldr.fix(0,4,1)"foldr/a T (a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a T) (λx,l0.a href="cic:/matita/basics/bool/if_then_else.def(1)"if_then_else/a ? (p x) (xa title="cons" href="cic:/fakeuri.def(1)":/a:l0) l0) a title="nil" href="cic:/fakeuri.def(1)"[/a].
+  a href="cic:/matita/tutorial/chapter3/foldr.fix(0,4,1)"foldr/a T (a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a T) (λx,l0. if p x then xa title="cons" href="cic:/fakeuri.def(1)":/a:l0 else l0) a title="nil" href="cic:/fakeuri.def(1)"[/a].
 
 (* Here are a couple of simple lemmas on the behaviour of the filter function. 
 It is often convenient to state such lemmas, in order to be able to use rewriting
@@ -265,7 +265,7 @@ that essentially allow you to iterate on every subset of a given enumerated
  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)" title="null"bool/a) (f:A→B) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) on l:B ≝  
  match l with 
   [ nil ⇒ b 
-  | cons a l ⇒ a href="cic:/matita/basics/bool/if_then_else.def(1)"if_then_else/a ? (p a) (op (f a) (fold A B op b p f l))
+  | cons a l ⇒ if p a then op (f a) (fold A B op b p f l) else
       (fold A B op b p f l)].
 
 (* It is also important to spend a few time to introduce some fancy notation
diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 55e734d56..be8ddaa59 100644
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -14,7 +14,7 @@ interpretation "empty set" 'empty_set = (empty_set ?).
 (* Similarly, a singleton set contaning containing an element a, is defined
 by by the characteristic function asserting equality with a *)
 
-definition singleton ≝ λA.λx,a:A.xa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa.
+definition singleton ≝ λA.λx,a:A.xa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aspan class="error" title="Parse error: [term] expected after [sym=] (in [term])"/spana.
 (* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
 interpretation "singleton" 'singl x = (singleton ? x).
 
@@ -27,7 +27,7 @@ conjunction and negation *)
 definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a a title="logical or" href="cic:/fakeuri.def(1)"∨/a Q a.
 interpretation "union" 'union a b = (union ? a b).
 
-definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a a title="logical and" href="cic:/fakeuri.def(1)"∧/a Q a.
+definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a a title="logical and" href="cic:/fakeuri.def(1)"∧/aspan class="error" title="Parse error: [term] expected after [sym∧] (in [term])"/span Q a.
 interpretation "intersection" 'intersects a b = (intersection ? a b).
 
 definition complement ≝ λU:Type[0].λA:U → Prop.λw.a title="logical not" href="cic:/fakeuri.def(1)"¬/a A w.
@@ -45,7 +45,7 @@ interpretation "subset" 'subseteq a b = (subset ? a b).
 (* Two sets are equals if and only if they have the same elements, that is,
 if the two characteristic functions are extensionally equivalent: *) 
 
-definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a a title="iff" href="cic:/fakeuri.def(1)"↔/a Q a.
+definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a a title="iff" href="cic:/fakeuri.def(1)"↔/aspan class="error" title="Parse error: [term] expected after [sym↔] (in [term])"/span Q a.
 notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
 
@@ -65,7 +65,7 @@ lemma eqP_trans: ∀U.∀A,B,C:U →Prop.
 with respect to eqP: *)
 
 lemma eqP_union_r: ∀U.∀A,B,C:U →Prop. 
-  A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C  → A a title="union" href="cic:/fakeuri.def(1)"∪/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C a title="union" href="cic:/fakeuri.def(1)"∪/a B.
+  A a title="extensional equality" href="cic:/fakeuri.def(1)"=/aspan class="error" title="Parse error: NUMBER '1' or [term] expected after [sym=] (in [term])"/span1 C  → A a title="union" href="cic:/fakeuri.def(1)"∪/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C a title="union" href="cic:/fakeuri.def(1)"∪/a B.
 #U #A #B #C #eqAB #a @a href="cic:/matita/basics/logic/iff_or_r.def(2)"iff_or_r/a @eqAB qed.
   
 lemma eqP_union_l: ∀U.∀A,B,C:U →Prop. 
@@ -77,7 +77,7 @@ lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop.
 #U #A #B #C #eqAB #a @a href="cic:/matita/basics/logic/iff_and_r.def(2)"iff_and_r/a @eqAB qed.
   
 lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop. 
-  B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C  → A a title="intersection" href="cic:/fakeuri.def(1)"∩/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="intersection" href="cic:/fakeuri.def(1)"∩/a C.
+  B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C  → A a title="intersection" href="cic:/fakeuri.def(1)"∩/aspan class="error" title="Parse error: [term] expected after [sym∩] (in [term])"/span B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="intersection" href="cic:/fakeuri.def(1)"∩/a C.
 #U #A #B #C #eqBC #a @a href="cic:/matita/basics/logic/iff_and_l.def(2)"iff_and_l/a @eqBC qed.
 
 lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop. 
@@ -103,7 +103,7 @@ lemma union_comm : ∀U.∀A,B:U →Prop.
 
 lemma union_assoc: ∀U.∀A,B,C:U → Prop. 
   A a title="union" href="cic:/fakeuri.def(1)"∪/a B a title="union" href="cic:/fakeuri.def(1)"∪/a C a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="union" href="cic:/fakeuri.def(1)"∪/a (B a title="union" href="cic:/fakeuri.def(1)"∪/a C).
-#S #A #B #C #w % [* [* /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ | /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/] | * [/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/ | * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/]
+#S #A #B #C #w % [* [* /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ | /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ ] | * [/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/ | * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/]
 qed.   
 
 (* In the same way we prove commutativity and associativity for set 
diff --git a/weblib/tutorial/chapter5.ma b/weblib/tutorial/chapter5.ma
index f9a0b30be..bc01f3c70 100644
--- a/weblib/tutorial/chapter5.ma
+++ b/weblib/tutorial/chapter5.ma
@@ -11,10 +11,10 @@ include "tutorial/chapter4.ma".
 between an element x and a list l. Its definition is a straightforward recursion on
 l.*)
 
-let rec memb (S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (x:S) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S) on l  ≝
+let rec memb (S:DeqSet) (x:S) (l: listspan class="error" title="Parse error: RPAREN expected after [term] (in [arg])"/span S) on l  ≝
   match l with
-  [ nil ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a
-  | cons a tl ⇒ (x a title="eqb" href="cic:/fakeuri.def(1)"=/a= a) a title="boolean or" href="cic:/fakeuri.def(1)"∨/a memb S x tl
+  [ nil ⇒ false
+  | cons a tl ⇒ (x =span class="error" title="Parse error: NUMBER '1' or [term] or [sym=] expected after [sym=] (in [term])"/span= a) ∨ memb S x tl
   ].
 
 notation < "\memb x l" non associative with precedence 90 for @{'memb $x $l}.
@@ -35,71 +35,71 @@ interpretation "boolean membership" 'memb a l = (memb ? a l).
   (op a b) is a member of (compose op l1 l2)
 *)
 
-lemma memb_hd: ∀S,a,l. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
-#S #a #l normalize >(a href="cic:/matita/basics/logic/proj2.def(2)"proj2/a … (a href="cic:/matita/tutorial/chapter4/eqb_true.fix(0,0,4)"eqb_true/a S …) (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a S a)) //
+lemma memb_hd: ∀S,a,l. memb S a (a::l) = true.
+#S #a #l normalize >(proj2 … (eqb_true S …) (refl S a)) //
 qed.
 
 lemma memb_cons: ∀S,a,b,l. 
-  a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l 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/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (ba title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
-#S #a #b #l normalize cases (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b) normalize // 
+  memb S a l = true → memba href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"/a S a (b::l) = true.
+#S #a #b #l normalize cases (a==b) normalize // 
 qed.
 
-lemma memb_single: ∀S,a,x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (xa 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 href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x.
-#S #a #x normalize cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a … (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=x)) #H
-  [#_ >(\P H) // |>H normalize #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/]
+lemma memb_single: ∀S,a,x. memb S a (x::[]) = true → a = x.
+#S #a #x normalize cases (true_or_false … (a==x)) #H
+  [#_ >(\P H) // |>H normalize #abs @False_ind /span class="autotactic"2span class="autotrace" trace absurd/span/span/]
 qed.
 
 lemma memb_append: ∀S,a,l1,l2. 
-a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (l1a title="append" href="cic:/fakeuri.def(1)"@/al2) 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/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l1a 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="logical or" href="cic:/fakeuri.def(1)"∨/a a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+memb S a (l1@a title="append" href="cic:/fakeuri.def(1)"/al2) = true → memb S a l1= true ∨ memb S a l2 = true.
 #S #a #l1 elim l1 normalize [#l2 #H %2 //] 
-#b #tl #Hind #l2 cases (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b) normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a/span/span/ 
+#b #tl #Hind #l2 cases (a==b) normalize /span class="autotactic"2span class="autotrace" trace orb_true_l/span/span/ 
 qed. 
 
 lemma memb_append_l1: ∀S,a,l1,l2. 
- a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l1a 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/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (l1a title="append" href="cic:/fakeuri.def(1)"@/al2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+ memb S a l1= true → memb S a (l1@a title="append" href="cic:/fakeuri.def(1)"/al2) = true.
 #S #a #l1 elim l1 normalize
-  [normalize #le #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
-  |#b #tl #Hind #l2 cases (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b) normalize /span class="autotactic"2span class="autotrace" trace /span/span/ 
+  [normalize #le #abs @False_ind /span class="autotactic"2span class="autotrace" trace absurd/span/span/
+  |#b #tl #Hind #l2 cases (a==b) normalize /span class="autotactic"2span class="autotrace" trace /span/span/ 
   ]
 qed. 
 
 lemma memb_append_l2: ∀S,a,l1,l2. 
- a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l2a 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/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (l1a title="append" href="cic:/fakeuri.def(1)"@/al2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+ memb S a l2= true → memb S a (l1@l2) = true.
 #S #a #l1 elim l1 normalize //
-#b #tl #Hind #l2 cases (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b) normalize /span class="autotactic"2span class="autotrace" trace /span/span/ 
+#b #tl #Hind #l2 cases (a==b) normalize /span class="autotactic"2span class="autotrace" trace /span/span/ 
 qed. 
 
-lemma memb_exists: ∀S,a,l.a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l 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="exists" href="cic:/fakeuri.def(1)"∃/al1,l2.la title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/al1a title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:l2).
-#S #a #l elim l [normalize #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/]
-#b #tl #Hind #H cases (a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a … H)
-  [#eqba @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a S)) @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … tl) >(\P eqba) //
+lemma memb_exists: ∀S,a,l.memb S a l = truea href="cic:/matita/basics/bool/bool.con(0,1,0)"/a → ∃l1,l2.l=l1@(a::l2).
+#S #a #l elim l [normalize #abs @False_ind /span class="autotactic"2span class="autotrace" trace absurd/span/span/]
+#b #tl #Hind #H cases (orb_true_l … H)
+  [#eqba @(ex_intro … (nil S)) @(ex_intro … tl) >(\P eqba) //
   |#mem_tl cases (Hind mem_tl) #l1 * #l2 #eqtl
-   @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (ba title="cons" href="cic:/fakeuri.def(1)":/a:l1)) @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … l2) >eqtl //
+   @(ex_intro … (b::l1)) @(ex_intro … l2) >eqtl //
   ]
 qed.
 
 lemma not_memb_to_not_eq: ∀S,a,b,l. 
- a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l 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/tutorial/chapter5/memb.fix(0,2,4)"memb/a S b l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
-#S #a #b #l cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b)) // 
-#eqab >(\P eqab) #H >H #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
+ memb S a l = falsea href="cic:/matita/basics/bool/bool.con(0,2,0)"/a → memb S b l = true → a==b = false.
+#S #a #b #l cases (true_or_false (a==b)) // 
+#eqab >(\P eqab) #H >H #abs @False_ind /span class="autotactic"2span class="autotrace" trace absurd/span/span/
 qed. 
  
-lemma memb_map: ∀S1,S2,f,a,l. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S1 a la 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/tutorial/chapter5/memb.fix(0,2,4)"memb/a S2 (f a) (a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a … f l) 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 memb_map: ∀S1,S2,f,a,l. memb S1 a l= true → 
+  memb S2 (f a) (map … f l) =a title="leibnitz's equality" href="cic:/fakeuri.def(1)"/a true.
 #S1 #S2 #f #a #l elim l normalize [//]
-#x #tl #memba cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=x))
-  [#eqx >eqx >(\P eqx) >(\b (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a … (f x))) normalize //
-  |#eqx >eqx cases (f aa title="eqb" href="cic:/fakeuri.def(1)"=/a=f x) normalize /span class="autotactic"2span class="autotrace" trace /span/span/
+#x #tl #memba cases (true_or_false (a==x))
+  [#eqx >eqx >(\P eqx) >(\b (refl … (f x))) normalize //
+  |#eqx >eqx cases (f a==f x) normalize /span class="autotactic"2span class="autotrace" trace /span/span/
   ]
 qed.
 
 lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2.   
-  a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S1 a1 l1 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/tutorial/chapter5/memb.fix(0,2,4)"memb/a S2 a2 l2 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/tutorial/chapter5/memb.fix(0,2,4)"memb/a S3 (op a1 a2) (a href="cic:/matita/basics/list/compose.def(2)"compose/a S1 S2 S3 op l1 l2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+  memb S1 a1 l1 = true → memb S2 a2 l2 = true →
+  memb S3 (op a1 a2) (compose S1 S2 S3 op l1 l2) = true.
 #S1 #S2 #S3 #op #a1 #a2 #l1 elim l1 [normalize //]
-#x #tl #Hind #l2 #memba1 #memba2 cases (a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a … memba1)
-  [#eqa1 >(\P eqa1) @a href="cic:/matita/tutorial/chapter5/memb_append_l1.def(5)"memb_append_l1/a @a href="cic:/matita/tutorial/chapter5/memb_map.def(5)"memb_map/a // 
-  |#membtl @a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"memb_append_l2/a @Hind //
+#x #tl #Hind #l2 #memba1 #memba2 cases (orb_true_la href="cic:/matita/basics/bool/orb_true_l.def(2)"/a … memba1)
+  [#eqa1 >(\P eqa1) @memb_append_l1 @memb_map // 
+  |#membtl @memb_append_l2 @Hind //
   ]
 qed.
 
@@ -108,84 +108,84 @@ to avoid duplications of elements. The following uniqueb check this property. *)
 
 (*************** unicity test *****************)
 
-let rec uniqueb (S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) l on l : a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝
+let rec uniqueb (S:DeqSet) l on l : bool ≝
   match l with 
-  [ nil ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a
-  | cons a tl ⇒ a href="cic:/matita/basics/bool/notb.def(1)"notb/a (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a tl) a title="boolean and" href="cic:/fakeuri.def(1)"∧/a uniqueb S tl
+  [ nil ⇒ true
+  | cons a tl ⇒ notb (memb S a tl) ∧ uniqueb S tl
   ].
 
 (* unique_append l1 l2 add l1 in fornt of l2, but preserving unicity *)
 
-let rec unique_append (S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (l1,l2: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S) on l1 ≝
+let rec unique_append (S:DeqSet) (l1,l2: list S) on l1 ≝
   match l1 with
   [ nil ⇒ l2
   | cons a tl ⇒ 
      let r ≝ unique_append S tl l2 in
-     if a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a r then r else aa title="cons" href="cic:/fakeuri.def(1)":/a:r
+     if memb S a r then r else a::r
   ].
 
-axiom unique_append_elim: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀P: S → Prop.∀l1,l2. 
-(∀x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → P x) → (∀x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → P x) →
-∀x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S l1 l2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → P x. 
+axiom unique_append_elim: ∀S:DeqSet.∀P: S → Prop.∀l1,l2. 
+(∀x. memb S x l1 =a title="leibnitz's equality" href="cic:/fakeuri.def(1)"/a true → P x) → (∀x. memb S x l2 = true → P x) →
+∀x. memb S x (unique_append S l1 l2) = true → P x. 
 
-lemma unique_append_unique: ∀S,l1,l2. a href="cic:/matita/tutorial/chapter5/uniqueb.fix(0,1,5)"uniqueb/a S l2 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/tutorial/chapter5/uniqueb.fix(0,1,5)"uniqueb/a S (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S l1 l2) 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 unique_append_unique: ∀S,l1,l2. uniqueb S l2 = true →
+  uniqueb S (unique_append S l1 l2) = true.
 #S #l1 elim l1 normalize // #a #tl #Hind #l2 #uniquel2
-cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a … (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S tl l2))) 
+cases (true_or_falsea href="cic:/matita/basics/bool/true_or_false.def(1)"/a … (memb S a (unique_append S tl l2))) 
 #H >H normalize [@Hind //] >H normalize @Hind //
 qed.
 
 (******************* sublist *******************)
 definition sublist ≝ 
-  λS,l1,l2.∀a. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l1 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/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+  λS,l1,l2.∀a. memb S a l1 = true → memb S a l2 = true.
 
 lemma sublist_length: ∀S,l1,l2. 
- a href="cic:/matita/tutorial/chapter5/uniqueb.fix(0,1,5)"uniqueb/a S l1 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/tutorial/chapter5/sublist.def(5)"sublist/a S l1 l2 → a title="norm" href="cic:/fakeuri.def(1)"|/al1| a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a title="norm" href="cic:/fakeuri.def(1)"|/al2|.
+ uniqueb S l1 = true → sublist S l1 l2 → |l1| ≤ |l2|.
 #S #l1 elim l1 // 
 #a #tl #Hind #l2 #unique #sub
-cut (a title="exists" href="cic:/fakeuri.def(1)"∃/al3,l4.l2a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/al3a title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:l4)) [@a href="cic:/matita/tutorial/chapter5/memb_exists.def(5)"memb_exists/a @sub //]
-* #l3 * #l4 #eql2 >eql2 >a href="cic:/matita/basics/list/length_append.def(2)"length_append/a normalize 
-applyS a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a <a href="cic:/matita/basics/list/length_append.def(2)"length_append/a @Hind [@(a href="cic:/matita/basics/bool/andb_true_r.def(4)"andb_true_r/a … unique)]
+cut (∃a title="exists" href="cic:/fakeuri.def(1)"/al3,l4.l2=l3@(a::l4)) [@memb_exists @sub //]
+* #l3 * #l4 #eql2 >eql2 >length_append normalize 
+applyS le_S_S <length_append @Hind [@(andb_true_r … unique)]
 >eql2 in sub; #sub #x #membx 
-cases (a href="cic:/matita/tutorial/chapter5/memb_append.def(5)"memb_append/a … (sub x (a href="cic:/matita/basics/bool/orb_true_r2.def(3)"orb_true_r2/a … membx)))
-  [#membxl3 @a href="cic:/matita/tutorial/chapter5/memb_append_l1.def(5)"memb_append_l1/a //
-  |#membxal4 cases (a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a … membxal4)
-    [#eqxa @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a lapply (a href="cic:/matita/basics/bool/andb_true_l.def(4)"andb_true_l/a … unique)
-     <(\P eqxa) >membx normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ |#membxl4 @a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"memb_append_l2/a //
+cases (memb_append … (sub x (orb_true_r2 … membx)))
+  [#membxl3 @memb_append_l1 //
+  |#membxal4 cases (orb_true_l … membxal4)
+    [#eqxa @False_ind lapply (andb_true_l … unique)
+     <(\P eqxa) >membx normalize /span class="autotactic"2span class="autotrace" trace absurd/span/span/ |#membxl4 @memb_append_l2a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"/a //
     ]
   ]
 qed.
 
 lemma sublist_unique_append_l1: 
-  ∀S,l1,l2. a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S l1 (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S l1 l2).
-#S #l1 elim l1 normalize [#l2 #S #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/]
+  ∀S,l1,l2. sublist S l1 (unique_append S l1 l2).
+#S #l1 elim l1 normalize [#l2 #S #abs @False_ind /span class="autotactic"2span class="autotrace" trace absurd/span/span/]
 #x #tl #Hind #l2 #a 
-normalize cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a … (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=x)) #eqax >eqax 
-[<(\P eqax) cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S tl l2)))
-  [#H >H normalize // | #H >H normalize >(\b (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a … a)) //]
-|cases (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S tl l2)) normalize 
+normalize cases (true_or_false … (a==x)) #eqax >eqax 
+[<(\P eqax) cases (true_or_false (memb S a (unique_append S tl l2)))
+  [#H >H normalize // | #H >H normalize >(\b (refl … a)) //]
+|cases (memb S x (unique_append S tl l2)) normalize 
   [/span class="autotactic"2span class="autotrace" trace /span/span/ |>eqax normalize /span class="autotactic"2span class="autotrace" trace /span/span/]
 ]
 qed.
 
 lemma sublist_unique_append_l2: 
-  ∀S,l1,l2. a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S l2 (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S l1 l2).
+  ∀S,l1,l2. sublist S l2 (unique_append S l1 l2).
 #S #l1 elim l1 [normalize //] #x #tl #Hind normalize 
-#l2 #a cases (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S tl l2)) normalize
-[@Hind | cases (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=x) normalize // @Hind]
+#l2 #a cases (memb S x (unique_appenda href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"/a S tl l2)) normalize
+[@Hind | cases (a==x) normalize // @Hind]
 qed.
 
 lemma decidable_sublist:∀S,l1,l2. 
-  (a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S l1 l2) a title="logical or" href="cic:/fakeuri.def(1)"∨/a a title="logical not" href="cic:/fakeuri.def(1)"¬/a(a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S l1 l2).
+  (sublist S l1 l2) ∨ ¬(sublist S l1 l2).
 #S #l1 #l2 elim l1 
-  [%1 #a normalize in ⊢ (%→?); #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
+  [%1 #a normalize in ⊢ (%→?); #abs @False_ind /span class="autotactic"2span class="autotrace" trace absurd/span/span/
   |#a #tl * #subtl 
-    [cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l2)) #memba
-      [%1 whd #x #membx cases (a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a … membx)
+    [cases (true_or_false (memb S a l2)) #memba
+      [%1 whd #x #membx cases (orb_true_l … membx)
         [#eqax >(\P eqax) // |@subtl]
-      |%2 @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"eqnot_to_noteq/a … a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a memba)) #H1 @H1 @a href="cic:/matita/tutorial/chapter5/memb_hd.def(5)"memb_hd/a
+      |%2 @(not_to_not … (eqnot_to_noteq … true memba)) #H1 @H1 @memb_hd
       ]
-    |%2 @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … subtl) #H1 #x #H2 @H1 @a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"memb_cons/a //
+    |%2 @(not_to_not … subtl) #H1 #x #H2 @H1 @memb_consa href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"/a //
     ] 
   ]
 qed.
@@ -193,38 +193,38 @@ qed.
 (********************* filtering *****************)
 
 lemma filter_true: ∀S,f,a,l. 
-  a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (a href="cic:/matita/basics/list/filter.def(2)"filter/a S f l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → f 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.
-#S #f #a #l elim l [normalize #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/]
-#b #tl #Hind cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (f b)) #H
+  memb S a (filter S f l) = true → f a = true.
+#S #f #a #l elim l [normalize #H @False_ind /span class="autotactic"2span class="autotrace" trace absurd/span/span/]
+#b #tl #Hind cases (true_or_false (f b)) #H
 normalize >H normalize [2:@Hind]
-cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b)) #eqab
+cases (true_or_false (a==b)) #eqab
   [#_ >(\P eqab) // | >eqab normalize @Hind]
 qed. 
   
 lemma memb_filter_memb: ∀S,f,a,l. 
-  a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (a href="cic:/matita/basics/list/filter.def(2)"filter/a S f l) 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/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+  memb S a (filter S f l) = true → memba href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"/a S a l = true.
 #S #f #a #l elim l [normalize //]
 #b #tl #Hind normalize (cases (f b)) normalize 
-cases (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b) normalize // @Hind
+cases (a==b) normalize // @Hind
 qed.
   
-lemma memb_filter: ∀S,f,l,x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x (a href="cic:/matita/basics/list/filter.def(2)"filter/a ? f l) 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/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x l 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="logical and" href="cic:/fakeuri.def(1)"∧/a (f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a).
-/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a, a href="cic:/matita/tutorial/chapter5/filter_true.def(5)"filter_true/a, a href="cic:/matita/tutorial/chapter5/memb_filter_memb.def(5)"memb_filter_memb/a/span/span/ qed.
+lemma memb_filter: ∀S,f,l,x. memb S x (filter ? f l) = true → 
+memb S x l = true ∧ (f x = true).
+/span class="autotactic"3span class="autotrace" trace conj, filter_true, memb_filter_memba href="cic:/matita/tutorial/chapter5/memb_filter_memb.def(5)"/a/span/span/ qed.
 
-lemma memb_filter_l: ∀S,f,x,l. (f x 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/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x l 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/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x (a href="cic:/matita/basics/list/filter.def(2)"filter/a ? f l) 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 memb_filter_l: ∀S,f,x,l. (f x = true) → memb S x l = true →
+memb S x (filter ? f l) = true.
 #S #f #x #l #fx elim l normalize //
-#b #tl #Hind cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (xa title="eqb" href="cic:/fakeuri.def(1)"=/a=b)) #eqxb
-  [<(\P eqxb) >(\b (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a … x)) >fx normalize >(\b (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a … x)) normalize //
+#b #tl #Hind cases (true_or_false (x==b)) #eqxb
+  [<(\P eqxb) >(\b (refl … x)) >fx normalize >(\b (refl … x)) normalize //
   |>eqxb cases (f b) normalize [>eqxb normalize @Hind| @Hind]
   ]
 qed. 
 
 (********************* exists *****************)
 
-let rec exists (A:Type[0]) (p:A → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l : a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝
+let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : boola href="cic:/matita/basics/bool/bool.ind(1,0,0)"/a ≝
 match l with
-[ nil ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a
-| cons h t ⇒ a href="cic:/matita/basics/bool/orb.def(1)"orb/a (p h) (exists A p t)
+[ nil ⇒ false
+| cons h t ⇒ orb (p h) (exists A p t)
 ].
\ No newline at end of file