From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Fri, 6 Jul 2012 14:02:50 +0000 (+0000)
Subject: reverted to previous version (plus anchors)
X-Git-Tag: make_still_working~1616
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=80b2ee96ffe418af9c39d3714e2a2f1dc74dab41

reverted to previous version (plus anchors)
---

diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma
index d45b0121b..6927d4c99 100644
--- a/weblib/arithmetics/nat.ma
+++ b/weblib/arithmetics/nat.ma
@@ -560,7 +560,7 @@ monotonic_lt_plus_l. *)
 
 img class="anchor" src="icons/tick.png" id="lt_plus"theorem lt_plus: ∀n,m,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → p a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a q → n a title="natural plus" href="cic:/fakeuri.def(1)"+/a p a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m a title="natural plus" href="cic:/fakeuri.def(1)"+/a q.
 #n #m #p #q #ltnm #ltpq
-@(a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a ? (na title="natural plus" href="cic:/fakeuri.def(1)"+/aq)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(5)"monotonic_lt_plus_l/a, a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"monotonic_le_plus_r/a/span/span/ qed.
+@(a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a ? (na title="natural plus" href="cic:/fakeuri.def(1)"+/aq))/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"monotonic_le_plus_r/a, a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(9)"monotonic_lt_plus_l/a/span/span/ qed.
 
 img class="anchor" src="icons/tick.png" id="lt_plus_to_lt_l"theorem lt_plus_to_lt_l :∀n,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. pa title="natural plus" href="cic:/fakeuri.def(1)"+/an a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a qa title="natural plus" href="cic:/fakeuri.def(1)"+/an → pa title="natural 'less than'" href="cic:/fakeuri.def(1)"</aq.
 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_to_le.def(5)"le_plus_to_le/a/span/span/ qed.
@@ -687,14 +687,14 @@ qed. *)
   ∀c:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/lt.def(1)"lt/a (λt.(ca title="natural times" href="cic:/fakeuri.def(1)"*/at)).
 #c #posc #n #m #ltnm
 (elim ltnm) normalize
-  [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(5)"monotonic_lt_plus_l/a/span/span/
+  [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(9)"monotonic_lt_plus_l/a/span/span/ 
   |#a #_ #lt1 @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … lt1) //
   ]
 qed.
 
 img class="anchor" src="icons/tick.png" id="monotonic_lt_times_l"theorem monotonic_lt_times_l: 
   ∀c:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/lt.def(1)"lt/a (λt.(ta title="natural times" href="cic:/fakeuri.def(1)"*/ac)).
-/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_lt_times_r.def(9)"monotonic_lt_times_r/a/span/span/
+/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_lt_times_r.def(10)"monotonic_lt_times_r/a/span/span/
 qed.
 
 img class="anchor" src="icons/tick.png" id="lt_to_le_to_lt_times"theorem lt_to_le_to_lt_times: 
@@ -702,12 +702,12 @@ qed.
 #n #m #p #q #ltnm #lepq #posq
 @(a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"le_to_lt_to_lt/a ? (na title="natural times" href="cic:/fakeuri.def(1)"*/aq))
   [@a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a //
-  |@a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(10)"monotonic_lt_times_l/a //
+  |@a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(11)"monotonic_lt_times_l/a //
   ]
 qed.
 
 img class="anchor" src="icons/tick.png" id="lt_times"theorem lt_times:∀n,m,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="natural 'less than'" href="cic:/fakeuri.def(1)"</am → pa title="natural 'less than'" href="cic:/fakeuri.def(1)"</aq → na title="natural times" href="cic:/fakeuri.def(1)"*/ap a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a ma title="natural times" href="cic:/fakeuri.def(1)"*/aq.
-#n #m #p #q #ltnm #ltpq @a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(11)"lt_to_le_to_lt_times/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a, a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(5)"ltn_to_ltO/a/span/span/ 
+#n #m #p #q #ltnm #ltpq @a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(12)"lt_to_le_to_lt_times/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a, a href="cic:/matita/arithmetics/nat/ltn_to_ltO.def(5)"ltn_to_ltO/a/span/span/ 
 qed.
 
 img class="anchor" src="icons/tick.png" id="lt_times_n_to_lt_l"theorem lt_times_n_to_lt_l: 
@@ -911,15 +911,15 @@ qed.
 
 img class="anchor" src="icons/tick.png" id="le_minus_to_plus"theorem le_minus_to_plus: ∀n,m,p. na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p → na title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a pa title="natural plus" href="cic:/fakeuri.def(1)"+/am.
 #n #m #p #lep @a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a
-  [|@a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(6)"le_plus_minus_m_m/a | @a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"monotonic_le_plus_l/a // ]
+  [|@a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(9)"le_plus_minus_m_m/a | @a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"monotonic_le_plus_l/a // ]
 qed.
 
 img class="anchor" src="icons/tick.png" id="le_minus_to_plus_r"theorem le_minus_to_plus_r: ∀a,b,c. c a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b → a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b a title="natural minus" href="cic:/fakeuri.def(1)"-/a c → a a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b.
-#a #b #c #Hlecb #H >(a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a … Hlecb) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_minus_to_plus.def(7)"le_minus_to_plus/a/span/span/
+#a #b #c #Hlecb #H >(a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a … Hlecb) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_minus_to_plus.def(10)"le_minus_to_plus/a/span/span/
 qed.
 
 img class="anchor" src="icons/tick.png" id="le_plus_to_minus"theorem le_plus_to_minus: ∀n,m,p. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a pa title="natural plus" href="cic:/fakeuri.def(1)"+/am → na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p.
-#n #m #p #lep /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_minus_l.def(5)"monotonic_le_minus_l/a/span/span/ qed.
+#n #m #p #lep /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_minus_l.def(9)"monotonic_le_minus_l/a/span/span/ qed.
 
 img class="anchor" src="icons/tick.png" id="le_plus_to_minus_r"theorem le_plus_to_minus_r: ∀a,b,c. a a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a c → a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a c a title="natural minus" href="cic:/fakeuri.def(1)"-/ab.
 #a #b #c #H @(a href="cic:/matita/arithmetics/nat/le_plus_to_le_r.def(6)"le_plus_to_le_r/a … b) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a/span/span/
@@ -927,37 +927,37 @@ qed.
 
 img class="anchor" src="icons/tick.png" id="lt_minus_to_plus"theorem lt_minus_to_plus: ∀a,b,c. a a title="natural minus" href="cic:/fakeuri.def(1)"-/a b a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c a title="natural plus" href="cic:/fakeuri.def(1)"+/a b.
 #a #b #c #H @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a 
-@(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a …H)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(7)"le_plus_to_minus_r/a/span/span/
+@(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a …H)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(10)"le_plus_to_minus_r/a/span/span/
 qed.
 
 img class="anchor" src="icons/tick.png" id="lt_minus_to_plus_r"theorem lt_minus_to_plus_r: ∀a,b,c. a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b a title="natural minus" href="cic:/fakeuri.def(1)"-/a c → a a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b.
-#a #b #c #H @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(7)"le_plus_to_minus/a …))
+#a #b #c #H @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(10)"le_plus_to_minus/a …))
 @a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a //
 qed.
 
 img class="anchor" src="icons/tick.png" id="lt_plus_to_minus"theorem lt_plus_to_minus: ∀n,m,p. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a pa title="natural plus" href="cic:/fakeuri.def(1)"+/am → na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p.
-#n #m #p #lenm #H normalize <a href="cic:/matita/arithmetics/nat/minus_Sn_m.def(5)"minus_Sn_m/a // @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(7)"le_plus_to_minus/a //
+#n #m #p #lenm #H normalize <a href="cic:/matita/arithmetics/nat/minus_Sn_m.def(5)"minus_Sn_m/a // @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(10)"le_plus_to_minus/a //
 qed.
 
 img class="anchor" src="icons/tick.png" id="lt_plus_to_minus_r"theorem lt_plus_to_minus_r: ∀a,b,c. a a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c a title="natural minus" href="cic:/fakeuri.def(1)"-/a b.
-#a #b #c #H @a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(7)"le_plus_to_minus_r/a //
+#a #b #c #H @a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(10)"le_plus_to_minus_r/a //
 qed. 
 
 img class="anchor" src="icons/tick.png" id="monotonic_le_minus_r"theorem monotonic_le_minus_r: 
 ∀p,q,n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. q a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p → na title="natural minus" href="cic:/fakeuri.def(1)"-/ap a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a na title="natural minus" href="cic:/fakeuri.def(1)"-/aq.
-#p #q #n #lepq @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(7)"le_plus_to_minus/a 
-@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … (a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(6)"le_plus_minus_m_m/a ? q)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"monotonic_le_plus_r/a/span/span/
+#p #q #n #lepq @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(10)"le_plus_to_minus/a 
+@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … (a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(9)"le_plus_minus_m_m/a ? q)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_plus_r.def(3)"monotonic_le_plus_r/a/span/span/
 qed.
 
 img class="anchor" src="icons/tick.png" id="eq_minus_O"theorem eq_minus_O: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
   n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.
-#n #m #lenm @(a href="cic:/matita/arithmetics/nat/le_n_O_elim.def(4)"le_n_O_elim/a (na title="natural minus" href="cic:/fakeuri.def(1)"-/am)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_minus_r.def(8)"monotonic_le_minus_r/a/span/span/
+#n #m #lenm @(a href="cic:/matita/arithmetics/nat/le_n_O_elim.def(4)"le_n_O_elim/a (na title="natural minus" href="cic:/fakeuri.def(1)"-/am)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_le_minus_r.def(11)"monotonic_le_minus_r/a/span/span/
 qed.
 
 img class="anchor" src="icons/tick.png" id="distributive_times_minus"theorem distributive_times_minus: a href="cic:/matita/basics/relations/distributive.def(1)"distributive/a ? a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a a href="cic:/matita/arithmetics/nat/minus.fix(0,0,1)"minus/a.
 #a #b #c
 (cases (a href="cic:/matita/arithmetics/nat/decidable_lt.def(7)"decidable_lt/a b c)) #Hbc
- [> a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"eq_minus_O/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/ >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"eq_minus_O/a // 
+ [> a href="cic:/matita/arithmetics/nat/eq_minus_O.def(12)"eq_minus_O/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/ >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(12)"eq_minus_O/a // 
   @a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/
  |@a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a (applyS a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"plus_to_minus/a) <a href="cic:/matita/arithmetics/nat/distributive_times_plus.def(7)"distributive_times_plus/a 
   @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a (applyS a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_lt_to_le.def(6)"not_lt_to_le/a/span/span/
@@ -969,7 +969,7 @@ cases (a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"decidable_le/a
   [@a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"plus_to_minus/a @a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"plus_to_minus/a <a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"associative_plus/a
    @a href="cic:/matita/arithmetics/nat/minus_to_plus.def(8)"minus_to_plus/a //
   |cut (n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a ma title="natural plus" href="cic:/fakeuri.def(1)"+/ap) [@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … (a href="cic:/matita/arithmetics/nat/le_n_Sn.def(1)"le_n_Sn/a …)) @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a //]
-   #H >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"eq_minus_O/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"eq_minus_O/a, a href="cic:/matita/arithmetics/nat/monotonic_le_minus_l.def(5)"monotonic_le_minus_l/a/span/span/ 
+   #H >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(12)"eq_minus_O/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/eq_minus_O.def(12)"eq_minus_O/a, a href="cic:/matita/arithmetics/nat/monotonic_le_minus_l.def(9)"monotonic_le_minus_l/a/span/span/ 
   ]
 qed.
 
@@ -1116,5 +1116,4 @@ normalize // qed.
 
 img class="anchor" src="icons/tick.png" id="to_max"lemma to_max: ∀i,n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i.
 #i #n #m #leni #lemi normalize (cases (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m)) 
-normalize // qed.
-
+normalize // qed.
\ No newline at end of file
diff --git a/weblib/basics/bool.ma b/weblib/basics/bool.ma
index d532c3186..43f0f8d05 100644
--- a/weblib/basics/bool.ma
+++ b/weblib/basics/bool.ma
@@ -92,10 +92,9 @@ match b1 with [ true ⇒ P a href="cic:/matita/basics/bool/bool.con(0,1,0)"tru
   | false ⇒  match b2 with [ true ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a | false ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a ]].
 
 notation > "'if' term 46 e 'then' term 46 t 'else' term 46 f" non associative with precedence 46
-(* notation > "£ term 46 e &amp; term 46 t &amp; term 46 f" non associative with precedence 46 *)
- for @{ 'ite $e $t $f }.
+ for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f]  }.
 notation < "hvbox('if' \nbsp term 46 e \nbsp break 'then' \nbsp term 46 t \nbsp break 'else' \nbsp term 49 f \nbsp)" non associative with precedence 46
- for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }. 
+ for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }.
 
 img class="anchor" src="icons/tick.png" id="bool_to_decidable_eq"theorem bool_to_decidable_eq: 
   ∀b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (b1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ab2).
@@ -104,4 +103,3 @@ notation < "hvbox('if' \nbsp term 46 e \nbsp break 'then' \nbsp term 46 t \nbsp
 img class="anchor" src="icons/tick.png" id="true_or_false"theorem true_or_false:
 ∀b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. b 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 or" 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.
 #b (cases b) /span class="autotactic"2span 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.
-