commit by user andrea

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index ab758c124f52fafb842e8e3bd4246b61346c2aa6..11eb476e0f9cfa119e7b196f07f591497979aadf 100644 (file)
--- 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 ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6,\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"\ 6ff\ 5/a\ 6〉
+[ O ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6\ 5span class="error" title="Parse error: [sym,] expected after [term level 19] (in [term])"\ 6\ 5/span\ 6,\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"\ 6ff\ 5/a\ 6〉
 | S a ⇒ \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6
    let p ≝ (div2 a) in
-   match (\ 5a href="cic:/matita/basics/types/snd.def(1)"\ 6snd\ 5/a\ 6 … p) with
-   [ tt ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/basics/types/fst.def(1)"\ 6fst\ 5/a\ 6 … p),\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"\ 6ff\ 5/a\ 6〉 
-   | ff ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/basics/types/fst.def(1)"\ 6fst\ 5/a\ 6 … p, \ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"\ 6tt\ 5/a\ 6〉
+   match (\ 5a href="cic:/matita/basics/types/snd.fix(0,2,1)"\ 6snd\ 5/a\ 6\ 5span class="error" title="Parse error: SYMBOL ':' or RPAREN expected after [term] (in [term])"\ 6\ 5/span\ 6 … p) with
+   [ tt ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/basics/types/fst.fix(0,2,1)"\ 6fst\ 5/a\ 6 … p),\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"\ 6ff\ 5/a\ 6〉 
+   | ff ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/basics/types/fst.fix(0,2,1)"\ 6fst\ 5/a\ 6 … p, \ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"\ 6tt\ 5/a\ 6〉
    ]
 ]. 
 
@@ -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:A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B. p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/basics/types/fst.def(1)"\ 6fst\ 5/a\ 6 … p,\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 … p〉.
+lemma surjective_pairing: ∀A,B.∀p:A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B. p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/basics/types/fst.fix(0,2,1)"\ 6fst\ 5/a\ 6 … p,\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6\ 5span class="error" title="Parse error: [sym〉] or [sym,] expected after [term level 19] (in [term])"\ 6\ 5/span\ 6 … p〉.
 #A #B * // qed.
 
 lemma div2SO: ∀n,q. \ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"\ 6div2\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6q,\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"\ 6ff\ 5/a\ 6〉 → \ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"\ 6div2\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6q,\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"\ 6tt\ 5/a\ 6〉.
 #n #q #H normalize >H normalize // qed.
 
-lemma div2S1: ∀n,q. \ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"\ 6div2\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6q,\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"\ 6tt\ 5/a\ 6〉 → \ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"\ 6div2\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 q,\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"\ 6ff\ 5/a\ 6〉.
+lemma div2S1: ∀n,q. \ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"\ 6div2\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6q,\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"\ 6tt\ 5/a\ 6〉 → \ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"\ 6div2\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym=] (in [term])"\ 6\ 5/span\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 q,\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"\ 6ff\ 5/a\ 6〉.
 #n #q #H normalize >H normalize // qed.
 
 lemma div2_ok: ∀n,q,r. \ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"\ 6div2\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6q,r〉 → n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"\ 6twice\ 5/a\ 6 q) (\ 5a href="cic:/matita/tutorial/chapter2/nat_of_bool.def(1)"\ 6nat_of_bool\ 5/a\ 6 r).
 #n elim n
   [#q #r normalize #H destruct //
   |#a #Hind #q #r 
-   cut (\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"\ 6div2\ 5/a\ 6 a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/basics/types/fst.def(1)"\ 6fst\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"\ 6div2\ 5/a\ 6 a), \ 5a href="cic:/matita/basics/types/snd.def(1)"\ 6snd\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"\ 6div2\ 5/a\ 6 a)〉) [//] 
-   cases (\ 5a href="cic:/matita/basics/types/snd.def(1)"\ 6snd\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"\ 6div2\ 5/a\ 6 a))
+   cut (\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"\ 6div2\ 5/a\ 6 a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/basics/types/fst.fix(0,2,1)"\ 6fst\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"\ 6div2\ 5/a\ 6 a), \ 5a href="cic:/matita/basics/types/snd.fix(0,2,1)"\ 6snd\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"\ 6div2\ 5/a\ 6 a)〉) [//] 
+   cases (\ 5a href="cic:/matita/basics/types/snd.fix(0,2,1)"\ 6snd\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"\ 6div2\ 5/a\ 6 a))
     [#H >(\ 5a href="cic:/matita/tutorial/chapter2/div2S1.def(3)"\ 6div2S1\ 5/a\ 6 … H) #H1 destruct @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 \ 5span style="text-decoration: underline;"\ 6>\ 5/span\ 6\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"\ 6add_S\ 5/a\ 6 whd in ⊢ (???%); <\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"\ 6add_S\ 5/a\ 6 @(Hind … H) 
     |#H >(\ 5a href="cic:/matita/tutorial/chapter2/div2SO.def(3)"\ 6div2SO\ 5/a\ 6 … H) #H1 destruct >\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"\ 6add_S\ 5/a\ 6 @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 @(Hind … H) 
     ]
@@ -248,7 +248,7 @@ definition qr_spec ≝ λn.λp.∀q,r. p \ 5a 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.\ 5a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,2)"\ 6 Sub\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6\ 5span style="text-decoration: underline;"\ 6\ 5a href="cic:/matita/tutorial/chapter2/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6\ 5/span\ 6) (\ 5a href="cic:/matita/tutorial/chapter2/qr_spec.def(3)"\ 6qr_spec\ 5/a\ 6 n) ≝ λn.
+definition div2P: ∀n. \ 5a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,2)"\ 6Sub\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6\ 5span style="text-decoration: underline;"\ 6\ 5a href="cic:/matita/tutorial/chapter2/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6\ 5/span\ 6) (\ 5a href="cic:/matita/tutorial/chapter2/qr_spec.def(3)"\ 6qr_spec\ 5/a\ 6 n) ≝ λn.
  \ 5a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"\ 6mk_Sub\ 5/a\ 6 ?? (\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"\ 6div2\ 5/a\ 6 n) (\ 5a href="cic:/matita/tutorial/chapter2/div2_ok.def(4)"\ 6div2_ok\ 5/a\ 6 n).
 
 (* But we can also try do directly build such an object *)
@@ -257,11 +257,11 @@ definition div2Pagain : ∀n.\ 5a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,
 #n elim n
   [@(\ 5a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"\ 6mk_Sub\ 5/a\ 6 … \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6,\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"\ 6ff\ 5/a\ 6〉) normalize #q #r #H destruct //
   |#a * #p #qrspec 
-   cut (p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/basics/types/fst.def(1)"\ 6fst\ 5/a\ 6 … p, \ 5a href="cic:/matita/basics/types/snd.def(1)"\ 6snd\ 5/a\ 6 … p〉) [//] 
-   cases (\ 5a href="cic:/matita/basics/types/snd.def(1)"\ 6snd\ 5/a\ 6 … p)
-    [#H @(\ 5a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"\ 6mk_Sub\ 5/a\ 6 … \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/basics/types/fst.def(1)"\ 6fst\ 5/a\ 6 … p),\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"\ 6ff\ 5/a\ 6〉) whd #q #r #H1 destruct @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 \ 5span style="text-decoration: underline;"\ 6>\ 5/span\ 6\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"\ 6add_S\ 5/a\ 6
+   cut (p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/basics/types/fst.fix(0,2,1)"\ 6fst\ 5/a\ 6 … p, \ 5a href="cic:/matita/basics/types/snd.fix(0,2,1)"\ 6snd\ 5/a\ 6 … p〉) [//] 
+   cases (\ 5a href="cic:/matita/basics/types/snd.fix(0,2,1)"\ 6snd\ 5/a\ 6 … p)
+    [#H @(\ 5a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"\ 6mk_Sub\ 5/a\ 6 … \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/basics/types/fst.fix(0,2,1)"\ 6fst\ 5/a\ 6 … p),\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"\ 6ff\ 5/a\ 6〉) whd #q #r #H1 destruct @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 \ 5span style="text-decoration: underline;"\ 6>\ 5/span\ 6\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"\ 6add_S\ 5/a\ 6
      whd in ⊢ (???%); <\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"\ 6add_S\ 5/a\ 6 @(qrspec … H)
-    |#H @(\ 5a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"\ 6mk_Sub\ 5/a\ 6 … \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/basics/types/fst.def(1)"\ 6fst\ 5/a\ 6 … p,\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"\ 6tt\ 5/a\ 6〉) whd #q #r #H1 destruct >\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"\ 6add_S\ 5/a\ 6 @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 @(qrspec … H) 
+    |#H @(\ 5a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"\ 6mk_Sub\ 5/a\ 6 … \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/basics/types/fst.fix(0,2,1)"\ 6fst\ 5/a\ 6 … p,\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"\ 6tt\ 5/a\ 6〉) whd #q #r #H1 destruct >\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"\ 6add_S\ 5/a\ 6 @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 @(qrspec … H) 
   ]
 qed.
 

diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma
index f7ad9155715878b850f9441dc9a1df70d4aaa716..3d7eb7a56f60b61b6e5a137787c71e94f72316f9 100644 (file)
--- a/weblib/tutorial/chapter3.ma
+++ b/weblib/tutorial/chapter3.ma
@@ -59,14 +59,14 @@ function.*)
 let rec append A (l1: \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) l2 on l1 ≝ 
   match l1 with
   [ nil ⇒  l2
-  | cons hd tl ⇒  hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: append A tl l2 ].
+  | cons hd tl ⇒  hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5span class="error" title="Parse error: [sym:] expected after [sym:] (in [term])"\ 6\ 5/span\ 6: 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:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A. \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
+example nil_append: ∀A.∀l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A. \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym[] (in [term])"\ 6\ 5/span\ 6] \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 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:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
+lemma append_nil: ∀A.∀l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5span class="error" title="Parse error: [term level 46] expected after [sym@] (in [term])"\ 6\ 5/span\ 6\ 5span class="error" title="Parse error: [term level 46] expected after [sym@] (in [term])"\ 6\ 5/span\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 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: \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0
 definition tail ≝  λA.λl: \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
   match l with [ nil ⇒  \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] | cons hd tl ⇒  tl].
 
-example ex_head: ∀A.∀a,d,l. \ 5a href="cic:/matita/tutorial/chapter3/head.def(1)"\ 6head\ 5/a\ 6 A (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) d \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a.
+example ex_head: ∀A.∀a,d,l. \ 5a href="cic:/matita/tutorial/chapter3/head.def(1)"\ 6head\ 5/a\ 6 A (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) d \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym=] (in [term])"\ 6\ 5/span\ 6\ 5span class="error" title="Parse error: [term] expected after [sym=] (in [term])"\ 6\ 5/span\ 6 a.
 #A #a #d #l normalize // qed.
 
 (* Problemi con la notazione *)
@@ -123,7 +123,7 @@ let rec nth n (A:Type[0]) (l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0
 example ex_length: \ 5a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"\ 6length\ 5/a\ 6 ? (\ 5a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"\ 6cons\ 5/a\ 6 ? \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
 normalize // qed.
 
-example ex_nth: \ 5a href="cic:/matita/tutorial/chapter3/nth.fix(0,0,2)"\ 6nth\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6) ? (\ 5a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"\ 6cons\ 5/a\ 6 ? (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6) (\ 5a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"\ 6cons\ 5/a\ 6 ? \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6])) \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
+example ex_nth: \ 5a href="cic:/matita/tutorial/chapter3/nth.fix(0,0,2)"\ 6nth\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6) ? (\ 5a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"\ 6cons\ 5/a\ 6 ? (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6) (\ 5a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"\ 6cons\ 5/a\ 6 ? \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym[] (in [term])"\ 6\ 5/span\ 6])) \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
 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 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
-  \ 5a href="cic:/matita/tutorial/chapter3/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 T (\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T) (λx,l0.\ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"\ 6if_then_else\ 5/a\ 6 ? (p x) (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l0) l0) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
+  \ 5a href="cic:/matita/tutorial/chapter3/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 T (\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T) (λx,l0. if p x then x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l0 else l0) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
 
 (* 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→\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"\ 6bool\ 5/a\ 6) (f:A→B) (l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l:B ≝  
  match l with 
   [ nil ⇒ b 
-  | cons a l ⇒ \ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"\ 6if_then_else\ 5/a\ 6 ? (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 55e734d56a5fa36cf400dea83b04bd70040c6a15..be8ddaa594212f9b0dacba4a7d7ddb8c81a23982 100644 (file)
--- 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.x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6a.
+definition singleton ≝ λA.λx,a:A.x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym=] (in [term])"\ 6\ 5/span\ 6a.
 (* 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 \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 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 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 Q a.
+definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym∧] (in [term])"\ 6\ 5/span\ 6 Q a.
 interpretation "intersection" 'intersects a b = (intersection ? a b).
 
 definition complement ≝ λU:Type[0].λA:U → Prop.λw.\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 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 \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 Q a.
+definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym↔] (in [term])"\ 6\ 5/span\ 6 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 \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C  → A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B.
+  A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5span class="error" title="Parse error: NUMBER '1' or [term] expected after [sym=] (in [term])"\ 6\ 5/span\ 61 C  → A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B.
 #U #A #B #C #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_or_r.def(2)"\ 6iff_or_r\ 5/a\ 6 @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 @\ 5a href="cic:/matita/basics/logic/iff_and_r.def(2)"\ 6iff_and_r\ 5/a\ 6 @eqAB qed.
   
 lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop. 
-  B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C  → A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 C.
+  B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C  → A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym∩] (in [term])"\ 6\ 5/span\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 C.
 #U #A #B #C #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_and_l.def(2)"\ 6iff_and_l\ 5/a\ 6 @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 \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 C \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 (B \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 C).
-#S #A #B #C #w % [* [* /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] | * [/\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
+#S #A #B #C #w % [* [* /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ ] | * [/\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
 qed.   
 
 (* In the same way we prove commutativity and associativity for set 

diff --git a/weblib/tutorial/chapter5.ma b/weblib/tutorial/chapter5.ma
index f9a0b30be8fc40a1d30f69425f841df1777c8482..bc01f3c7021d350d8a490f3e5fb99f1aabbbfe32 100644 (file)
--- 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:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (x:S) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S) on l  ≝
+let rec memb (S:DeqSet) (x:S) (l: list\ 5span class="error" title="Parse error: RPAREN expected after [term] (in [arg])"\ 6\ 5/span\ 6 S) on l  ≝
   match l with
-  [ nil ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
-  | cons a tl ⇒ (x \ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6= a) \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 memb S x tl
+  [ nil ⇒ false
+  | cons a tl ⇒ (x =\ 5span class="error" title="Parse error: NUMBER '1' or [term] or [sym=] expected after [sym=] (in [term])"\ 6\ 5/span\ 6= 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. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
-#S #a #l normalize >(\ 5a href="cic:/matita/basics/logic/proj2.def(2)"\ 6proj2\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter4/eqb_true.fix(0,0,4)"\ 6eqb_true\ 5/a\ 6 S …) (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 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. 
-  \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (b\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
-#S #a #b #l normalize cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b) normalize // 
+  memb S a l = true → memb\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6\ 5/a\ 6 S a (b::l) = true.
+#S #a #b #l normalize cases (a==b) normalize // 
 qed.
 
-lemma memb_single: ∀S,a,x. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x.
-#S #a #x normalize cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 … (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=x)) #H
-  [#_ >(\P H) // |>H normalize #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
+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 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/]
 qed.
 
 lemma memb_append: ∀S,a,l1,l2. 
-\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l1\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+memb S a (l1@\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6l2) = 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 (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ 
+#b #tl #Hind #l2 cases (a==b) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace orb_true_l\ 5/span\ 6\ 5/span\ 6/ 
 qed. 
 
 lemma memb_append_l1: ∀S,a,l1,l2. 
- \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l1\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+ memb S a l1= true → memb S a (l1@\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6l2) = true.
 #S #a #l1 elim l1 normalize
-  [normalize #le #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
-  |#b #tl #Hind #l2 cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ 
+  [normalize #le #abs @False_ind /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/
+  |#b #tl #Hind #l2 cases (a==b) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ 
   ]
 qed. 
 
 lemma memb_append_l2: ∀S,a,l1,l2. 
- \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l2\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+ memb S a l2= true → memb S a (l1@l2) = true.
 #S #a #l1 elim l1 normalize //
-#b #tl #Hind #l2 cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ 
+#b #tl #Hind #l2 cases (a==b) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ 
 qed. 
 
-lemma memb_exists: ∀S,a,l.\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6l1,l2.l\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l2).
-#S #a #l elim l [normalize #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
-#b #tl #Hind #H cases (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … H)
-  [#eqba @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 S)) @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … tl) >(\P eqba) //
+lemma memb_exists: ∀S,a,l.memb S a l = true\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6\ 5/a\ 6 → ∃l1,l2.l=l1@(a::l2).
+#S #a #l elim l [normalize #abs @False_ind /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/]
+#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
-   @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (b\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l1)) @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … l2) >eqtl //
+   @(ex_intro … (b::l1)) @(ex_intro … l2) >eqtl //
   ]
 qed.
 
 lemma not_memb_to_not_eq: ∀S,a,b,l. 
- \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S b l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
-#S #a #b #l cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b)) // 
-#eqab >(\P eqab) #H >H #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ memb S a l = false\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6\ 5/a\ 6 → 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 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/
 qed. 
  
-lemma memb_map: ∀S1,S2,f,a,l. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S1 a l\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → 
-  \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S2 (f a) (\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 … f l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+lemma memb_map: ∀S1,S2,f,a,l. memb S1 a l= true → 
+  memb S2 (f a) (map … f l) =\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 true.
 #S1 #S2 #f #a #l elim l normalize [//]
-#x #tl #memba cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=x))
-  [#eqx >eqx >(\P eqx) >(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 … (f x))) normalize //
-  |#eqx >eqx cases (f a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=f x) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+#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 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
   ]
 qed.
 
 lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2.   
-  \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S1 a1 l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S2 a2 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
-  \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S3 (op a1 a2) (\ 5a href="cic:/matita/basics/list/compose.def(2)"\ 6compose\ 5/a\ 6 S1 S2 S3 op l1 l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+  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 (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … memba1)
-  [#eqa1 >(\P eqa1) @\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l1.def(5)"\ 6memb_append_l1\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter5/memb_map.def(5)"\ 6memb_map\ 5/a\ 6 // 
-  |#membtl @\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"\ 6memb_append_l2\ 5/a\ 6 @Hind //
+#x #tl #Hind #l2 #memba1 #memba2 cases (orb_true_l\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6\ 5/a\ 6 … 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:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) l on l : \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
+let rec uniqueb (S:DeqSet) l on l : bool ≝
   match l with 
-  [ nil ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6
-  | cons a tl ⇒ \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a tl) \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 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:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (l1,l2: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 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 \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a r then r else a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:r
+     if memb S a r then r else a::r
   ].
 
-axiom unique_append_elim: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀P: S → Prop.∀l1,l2. 
-(∀x. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → P x) → (∀x. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → P x) →
-∀x. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S l1 l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → P x. 
+axiom unique_append_elim: ∀S:DeqSet.∀P: S → Prop.∀l1,l2. 
+(∀x. memb S x l1 =\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 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. \ 5a href="cic:/matita/tutorial/chapter5/uniqueb.fix(0,1,5)"\ 6uniqueb\ 5/a\ 6 S l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
-  \ 5a href="cic:/matita/tutorial/chapter5/uniqueb.fix(0,1,5)"\ 6uniqueb\ 5/a\ 6 S (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S l1 l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+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 (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S tl l2))) 
+cases (true_or_false\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6\ 5/a\ 6 … (memb S a (unique_append S tl l2))) 
 #H >H normalize [@Hind //] >H normalize @Hind //
 qed.
 
 (******************* sublist *******************)
 definition sublist ≝ 
-  λS,l1,l2.∀a. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+  λS,l1,l2.∀a. memb S a l1 = true → memb S a l2 = true.
 
 lemma sublist_length: ∀S,l1,l2. 
- \ 5a href="cic:/matita/tutorial/chapter5/uniqueb.fix(0,1,5)"\ 6uniqueb\ 5/a\ 6 S l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 S l1 l2 → \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l1| \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l2|.
+ uniqueb S l1 = true → sublist S l1 l2 → |l1| ≤ |l2|.
 #S #l1 elim l1 // 
 #a #tl #Hind #l2 #unique #sub
-cut (\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6l3,l4.l2\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6l3\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l4)) [@\ 5a href="cic:/matita/tutorial/chapter5/memb_exists.def(5)"\ 6memb_exists\ 5/a\ 6 @sub //]
-* #l3 * #l4 #eql2 >eql2 >\ 5a href="cic:/matita/basics/list/length_append.def(2)"\ 6length_append\ 5/a\ 6 normalize 
-applyS \ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 <\ 5a href="cic:/matita/basics/list/length_append.def(2)"\ 6length_append\ 5/a\ 6 @Hind [@(\ 5a href="cic:/matita/basics/bool/andb_true_r.def(4)"\ 6andb_true_r\ 5/a\ 6 … unique)]
+cut (∃\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6l3,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 (\ 5a href="cic:/matita/tutorial/chapter5/memb_append.def(5)"\ 6memb_append\ 5/a\ 6 … (sub x (\ 5a href="cic:/matita/basics/bool/orb_true_r2.def(3)"\ 6orb_true_r2\ 5/a\ 6 … membx)))
-  [#membxl3 @\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l1.def(5)"\ 6memb_append_l1\ 5/a\ 6 //
-  |#membxal4 cases (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … membxal4)
-    [#eqxa @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 lapply (\ 5a href="cic:/matita/basics/bool/andb_true_l.def(4)"\ 6andb_true_l\ 5/a\ 6 … unique)
-     <(\P eqxa) >membx normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ |#membxl4 @\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"\ 6memb_append_l2\ 5/a\ 6 //
+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 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/ |#membxl4 @memb_append_l2\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"\ 6\ 5/a\ 6 //
     ]
   ]
 qed.
 
 lemma sublist_unique_append_l1: 
-  ∀S,l1,l2. \ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 S l1 (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S l1 l2).
-#S #l1 elim l1 normalize [#l2 #S #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
+  ∀S,l1,l2. sublist S l1 (unique_append S l1 l2).
+#S #l1 elim l1 normalize [#l2 #S #abs @False_ind /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/]
 #x #tl #Hind #l2 #a 
-normalize cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 … (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=x)) #eqax >eqax 
-[<(\P eqax) cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S tl l2)))
-  [#H >H normalize // | #H >H normalize >(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 … a)) //]
-|cases (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 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 
   [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ |>eqax normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/]
 ]
 qed.
 
 lemma sublist_unique_append_l2: 
-  ∀S,l1,l2. \ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 S l2 (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 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 (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S tl l2)) normalize
-[@Hind | cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=x) normalize // @Hind]
+#l2 #a cases (memb S x (unique_append\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6\ 5/a\ 6 S tl l2)) normalize
+[@Hind | cases (a==x) normalize // @Hind]
 qed.
 
 lemma decidable_sublist:∀S,l1,l2. 
-  (\ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 S l1 l2) \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 S l1 l2).
+  (sublist S l1 l2) ∨ ¬(sublist S l1 l2).
 #S #l1 #l2 elim l1 
-  [%1 #a normalize in ⊢ (%→?); #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+  [%1 #a normalize in ⊢ (%→?); #abs @False_ind /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/
   |#a #tl * #subtl 
-    [cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l2)) #memba
-      [%1 whd #x #membx cases (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … membx)
+    [cases (true_or_false (memb S a l2)) #memba
+      [%1 whd #x #membx cases (orb_true_l … membx)
         [#eqax >(\P eqax) // |@subtl]
-      |%2 @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … (\ 5a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"\ 6eqnot_to_noteq\ 5/a\ 6 … \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 memba)) #H1 @H1 @\ 5a href="cic:/matita/tutorial/chapter5/memb_hd.def(5)"\ 6memb_hd\ 5/a\ 6
+      |%2 @(not_to_not … (eqnot_to_noteq … true memba)) #H1 @H1 @memb_hd
       ]
-    |%2 @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … subtl) #H1 #x #H2 @H1 @\ 5a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"\ 6memb_cons\ 5/a\ 6 //
+    |%2 @(not_to_not … subtl) #H1 #x #H2 @H1 @memb_cons\ 5a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"\ 6\ 5/a\ 6 //
     ] 
   ]
 qed.
@@ -193,38 +193,38 @@ qed.
 (********************* filtering *****************)
 
 lemma filter_true: ∀S,f,a,l. 
-  \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 S f l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → f a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
-#S #f #a #l elim l [normalize #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
-#b #tl #Hind cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (f b)) #H
+  memb S a (filter S f l) = true → f a = true.
+#S #f #a #l elim l [normalize #H @False_ind /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/]
+#b #tl #Hind cases (true_or_false (f b)) #H
 normalize >H normalize [2:@Hind]
-cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b)) #eqab
+cases (true_or_false (a==b)) #eqab
   [#_ >(\P eqab) // | >eqab normalize @Hind]
 qed. 
   
 lemma memb_filter_memb: ∀S,f,a,l. 
-  \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 S f l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+  memb S a (filter S f l) = true → memb\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6\ 5/a\ 6 S a l = true.
 #S #f #a #l elim l [normalize //]
 #b #tl #Hind normalize (cases (f b)) normalize 
-cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b) normalize // @Hind
+cases (a==b) normalize // @Hind
 qed.
   
-lemma memb_filter: ∀S,f,l,x. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 ? f l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → 
-\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 (f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6).
-/\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter5/filter_true.def(5)"\ 6filter_true\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter5/memb_filter_memb.def(5)"\ 6memb_filter_memb\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
+lemma memb_filter: ∀S,f,l,x. memb S x (filter ? f l) = true → 
+memb S x l = true ∧ (f x = true).
+/\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace conj, filter_true, memb_filter_memb\ 5a href="cic:/matita/tutorial/chapter5/memb_filter_memb.def(5)"\ 6\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
 
-lemma memb_filter_l: ∀S,f,x,l. (f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
-\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 ? f l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+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 (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (x\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b)) #eqxb
-  [<(\P eqxb) >(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 … x)) >fx normalize >(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 … 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 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l : \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
+let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6\ 5/a\ 6 ≝
 match l with
-[ nil ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
-| cons h t ⇒ \ 5a href="cic:/matita/basics/bool/orb.def(1)"\ 6orb\ 5/a\ 6 (p h) (exists A p t)
+[ nil ⇒ false
+| cons h t ⇒ orb (p h) (exists A p t)
 ].
\ No newline at end of file