From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Tue, 6 Mar 2012 18:01:38 +0000 (+0000)
Subject: commit by user utente2
X-Git-Tag: make_still_working~1892
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a4c1fed77216ee3dfc19ce4f3a1d7dd82de10171;p=helm.git

commit by user utente2
---

diff --git a/weblib/tutorial/chapter7.ma b/weblib/tutorial/chapter7.ma
index 17316f031..55a830179 100644
--- a/weblib/tutorial/chapter7.ma
+++ b/weblib/tutorial/chapter7.ma
@@ -229,11 +229,11 @@ interpretation "in_prl" 'in_l E = (in_prl ? E).
 (* The following, trivial lemmas are only meant for rewriting purposes. *)
 
 lemma sem_pre_true : ∀S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. 
-  a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉} a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{i} a title="union" href="cic:/fakeuri.def(1)"∪/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a}. 
+  a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉} a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{i} a title="union" href="cic:/fakeuri.def(1)"∪/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a}. 
 // qed.
 
 lemma sem_pre_false : ∀S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. 
-  a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉} a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{i}. 
+  a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉} a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{i}. 
 // qed.
 
 lemma sem_cat: ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. 
diff --git a/weblib/tutorial/chapter8.ma b/weblib/tutorial/chapter8.ma
index 7462d74b7..a84d10a2a 100644
--- a/weblib/tutorial/chapter8.ma
+++ b/weblib/tutorial/chapter8.ma
@@ -13,7 +13,7 @@ reached the end of a + ϵ and we must pursue broadcasting inside (b*a + b)b. Aga
 parallel on the two additive subterms b^*a and b; the first point is allowed to both enter the 
 star, and to traverse it, stopping in front of a; the second point just stops in front of b. 
 No point reached that end of b^*a + b hence no further propagation is possible. In conclusion: 
-               •((a + ϵ)(b^*a + b)b) = 〈(•a + ϵ)((•b)^*•a + •b)b, false〉
+               •((a + ϵ)(b^*a + b)b) = 〈(•a + ϵ)((•b)^*•a + •b)b, false〉
 *)
 
 include "tutorial/chapter7.ma".
@@ -22,17 +22,17 @@ include "tutorial/chapter7.ma".
 the end of the expression. 
 Broadcasting inside a i1+i2 amounts to broadcast in parallel inside i1 and i2.
 If we define
-                 〈i1,b1〉 ⊕ 〈i2,b2〉 = 〈i1 + i2, b1∨ b2〉
+                 〈i1,b1〉 ⊕ 〈i2,b2〉 = 〈i1 + i2, b1∨ b2〉
 then, we just have •(i1+i2) = •(i1)⊕ •(i2).
 *)
 
 include "tutorial/chapter7.ma".
 
-definition lo ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λa,b:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a a a title="pitem or" href="cic:/fakeuri.def(1)"+/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a b,a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a a a title="boolean or" href="cic:/fakeuri.def(1)"∨/a a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a b〉.
+definition lo ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λa,b:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a a a title="pitem or" href="cic:/fakeuri.def(1)"+/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a b,a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a a a title="boolean or" href="cic:/fakeuri.def(1)"∨/a a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a b〉.
 notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
 interpretation "oplus" 'oplus a b = (lo ? a b).
 
-lemma lo_def: ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀b1,b2. a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,b1〉a title="oplus" href="cic:/fakeuri.def(1)"⊕/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai2,b2〉a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1a title="pitem or" href="cic:/fakeuri.def(1)"+/ai2,b1a title="boolean or" href="cic:/fakeuri.def(1)"∨/ab2〉.
+lemma lo_def: ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀b1,b2. a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,b1〉a title="oplus" href="cic:/fakeuri.def(1)"⊕/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai2,b2〉a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1a title="pitem or" href="cic:/fakeuri.def(1)"+/ai2,b1a title="boolean or" href="cic:/fakeuri.def(1)"∨/ab2〉.
 // qed.
 
 (*
@@ -42,15 +42,15 @@ point reached the end of i1. This suggests to define •(i1 · i2) as •(i1) 
 e ▹ i is a general operation of concatenation between a pre and an item, defined by 
 cases on the boolean in e: 
 
-       〈i1,true〉 ▹ i2  = i1 ◃ •(i_2)
-       〈i1,false〉 ▹ i2 = i1 · i2
+       〈i1,true〉 ▹ i2  = i1 ◃ •(i_2)
+       〈i1,false〉 ▹ i2 = i1 · i2
 In turn, ◃ says how to concatenate an item with a pre, that is however extremely simple:
-        i1 ◃ 〈i1,b〉  = 〈i_1 · i2, b〉
+        i1 ◃ 〈i1,b〉  = 〈i_1 · i2, b〉
 Let us come to the formalized definitions:
 *)
 
 definition pre_concat_r ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λi:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.λe:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.
-  match e with [ mk_Prod i1 b ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i1, b〉].
+  match e with [ mk_Prod i1 b ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i1, b〉].
  
 notation "i ◃ e" left associative with precedence 60 for @{'lhd $i $e}.
 interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e).
@@ -77,7 +77,7 @@ definition pre_concat_l ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.in
   match e1 with 
   [ mk_Prod i1 b1 ⇒ match b1 with 
     [ true ⇒ (i1 a title="pre_concat_r" href="cic:/fakeuri.def(1)"◃/a (bcast ? i2)) 
-    | false ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i2,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉
+    | false ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i2,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉
     ]
   ].
 
@@ -90,13 +90,13 @@ notation "•" non associative with precedence 60 for @{eclose ?}.
 
 let rec eclose (S: a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (i: a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S) on i : a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S ≝
  match i with
-  [ pz ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"pz/a ?, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a 〉
-  | pe ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pitem epsilon" href="cic:/fakeuri.def(1)"ϵ/a,  a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a 〉
-  | ps x ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pitem pp" href="cic:/fakeuri.def(1)"`/a.x, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉
-  | pp x ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pitem pp" href="cic:/fakeuri.def(1)"`/a.x, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a 〉
+  [ pz ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"pz/a ?, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a 〉
+  | pe ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pitem epsilon" href="cic:/fakeuri.def(1)"ϵ/a,  a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a 〉
+  | ps x ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pitem pp" href="cic:/fakeuri.def(1)"`/a.x, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉
+  | pp x ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pitem pp" href="cic:/fakeuri.def(1)"`/a.x, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a 〉
   | po i1 i2 ⇒ •i1 a title="oplus" href="cic:/fakeuri.def(1)"⊕/a •i2
   | pc i1 i2 ⇒ •i1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i2
-  | pk i ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (•i))a title="pitem star" href="cic:/fakeuri.def(1)"^/a*,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉].
+  | pk i ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (•i))a title="pitem star" href="cic:/fakeuri.def(1)"^/a*,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉].
   
 notation "• x" non associative with precedence 60 for @{'eclose $x}.
 interpretation "eclose" 'eclose x = (eclose ? x).
@@ -104,15 +104,15 @@ interpretation "eclose" 'eclose x = (eclose ? x).
 (* Here are a few simple properties of ▹ and •(-) *)
 
 lemma pcl_true : ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.
-  a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a i1 a title="pre_concat_r" href="cic:/fakeuri.def(1)"◃/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2).
+  a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a i1 a title="pre_concat_r" href="cic:/fakeuri.def(1)"◃/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2).
 // qed.
 
 lemma pcl_true_bis : ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.
-  a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2), a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2)〉.
+  a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2), a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2)〉.
 #S #i1 #i2 normalize cases (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2) // qed.
 
 lemma pcl_false: ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.
-  a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a  i2  a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i2, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉.
+  a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a  i2  a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i2, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉.
 // qed.
 
 lemma eclose_plus: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.
@@ -124,7 +124,7 @@ lemma eclose_dot: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
 // qed.
 
 lemma eclose_star: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.
-  a title="eclose" href="cic:/fakeuri.def(1)"•/aia title="pitem star" href="cic:/fakeuri.def(1)"^/a* a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a(a title="eclose" href="cic:/fakeuri.def(1)"•/ai))a title="pitem star" href="cic:/fakeuri.def(1)"^/a*,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉.
+  a title="eclose" href="cic:/fakeuri.def(1)"•/aia title="pitem star" href="cic:/fakeuri.def(1)"^/a* a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a(a title="eclose" href="cic:/fakeuri.def(1)"•/ai))a title="pitem star" href="cic:/fakeuri.def(1)"^/a*,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉.
 // qed.
 
 (* The definition of •(-) (eclose) can then be lifted from items to pres
@@ -132,7 +132,7 @@ in the obvious way. *)
 
 definition lift ≝ λS.λf:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S →a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.λe:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. 
   match e with 
-  [ mk_Prod i b ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (f i), a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (f i) a title="boolean or" href="cic:/fakeuri.def(1)"∨/a b〉].
+  [ mk_Prod i b ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (f i), a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (f i) a title="boolean or" href="cic:/fakeuri.def(1)"∨/a b〉].
   
 definition preclose ≝ λS. a href="cic:/matita/tutorial/chapter8/lift.def(2)"lift/a S (a href="cic:/matita/tutorial/chapter8/eclose.fix(0,1,4)"eclose/a S). 
 interpretation "preclose" 'eclose x = (preclose ? x).
@@ -290,12 +290,12 @@ notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}.
 interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2).
 
 lemma odot_true_b : ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀b. 
-  a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai2,b〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2)),a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2) a title="boolean or" href="cic:/fakeuri.def(1)"∨/a b〉.
+  a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai2,b〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2)),a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2) a title="boolean or" href="cic:/fakeuri.def(1)"∨/a b〉.
 #S #i1 #i2 #b normalize in ⊢ (??%?); cases (a title="eclose" href="cic:/fakeuri.def(1)"•/ai2) // 
 qed.
 
 lemma odot_false_b : ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀b.
-  a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai2,b〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i2 ,b〉.
+  a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai2,b〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i2 ,b〉.
 // 
 qed.
   
@@ -310,8 +310,8 @@ definition lk ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
   match e with 
   [ mk_Prod i1 b1 ⇒
     match b1 with 
-    [true ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter8/eclose.fix(0,1,4)"eclose/a ? i1))a title="pitem star" href="cic:/fakeuri.def(1)"^/a*, a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉
-    |false ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1a title="pitem star" href="cic:/fakeuri.def(1)"^/a*,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉
+    [true ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter8/eclose.fix(0,1,4)"eclose/a ? i1))a title="pitem star" href="cic:/fakeuri.def(1)"^/a*, a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉
+    |false ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1a title="pitem star" href="cic:/fakeuri.def(1)"^/a*,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉
     ]
   ]. 
 
@@ -320,11 +320,11 @@ interpretation "lk" 'lk a = (lk ? a).
 notation "a^⊛" non associative with precedence 90 for @{'lk $a}.
 
 lemma ostar_true: ∀S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.
-  a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉a title="lk" href="cic:/fakeuri.def(1)"^/a⊛ a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai))a title="pitem star" href="cic:/fakeuri.def(1)"^/a*, a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉.
+  a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉a title="lk" href="cic:/fakeuri.def(1)"^/a⊛ a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a title="eclose" href="cic:/fakeuri.def(1)"•/ai))a title="pitem star" href="cic:/fakeuri.def(1)"^/a*, a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉.
 // qed.
 
 lemma ostar_false: ∀S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.
-  a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉a title="lk" href="cic:/fakeuri.def(1)"^/a⊛ a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aia title="pitem star" href="cic:/fakeuri.def(1)"^/a*, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉.
+  a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉a title="lk" href="cic:/fakeuri.def(1)"^/a⊛ a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aia title="pitem star" href="cic:/fakeuri.def(1)"^/a*, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉.
 // qed.
   
 lemma erase_ostar: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.
@@ -332,9 +332,9 @@ lemma erase_ostar: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"
 #S * #i * // qed.
 
 lemma sem_odot_true: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀e1:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.∀i. 
-  a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i} a title="union" href="cic:/fakeuri.def(1)"∪/a a title="singleton" href="cic:/fakeuri.def(1)"{/a a title="nil" href="cic:/fakeuri.def(1)"[/a ] }.
+  a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i} a title="union" href="cic:/fakeuri.def(1)"∪/a a title="singleton" href="cic:/fakeuri.def(1)"{/a a title="nil" href="cic:/fakeuri.def(1)"[/a ] }.
 #S #e1 #i 
-cut (e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i), a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a(e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i) a title="boolean or" href="cic:/fakeuri.def(1)"∨/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉) [//]
+cut (e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i), a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a(e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i) a title="boolean or" href="cic:/fakeuri.def(1)"∨/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉) [//]
 #H >H cases (e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i) #i1 #b1 cases b1 
   [>a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"sem_pre_true/a @a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"eqP_trans/a [||@a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"eqP_sym/a @a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"union_assoc/a]
    @a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"eqP_union_l/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"eqP_sym/a/span/span/ 
@@ -343,9 +343,9 @@ cut (e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair
 qed.
 
 lemma eq_odot_false: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀e1:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.∀i. 
-  e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i.
+  e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i.
 #S #e1 #i  
-cut (e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i), a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a(e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i) a title="boolean or" href="cic:/fakeuri.def(1)"∨/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉) [//]
+cut (e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i), a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a(e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i) a title="boolean or" href="cic:/fakeuri.def(1)"∨/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉) [//]
 cases (e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a i) #i1 #b1 cases b1 #H @H
 qed.