X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Fbool.ma;fp=weblib%2Fbasics%2Fbool.ma;h=7762657aec90514366049386a6453b8f275ec1e8;hb=569ba7fe357918e3e83c3fe2d5a41070834c5b67;hp=43f0f8d051a16c388c1599f59ee7c649e24128ff;hpb=4a41f041869956a6c98418e6d06b3a2521a1fb2a;p=helm.git

diff --git a/weblib/basics/bool.ma b/weblib/basics/bool.ma
index 43f0f8d05..7762657ae 100644
--- a/weblib/basics/bool.ma
+++ b/weblib/basics/bool.ma
@@ -16,7 +16,6 @@ include "basics/relations.ma".
   | true : bool
   | false : bool.
 
-(* destruct does not work *)
 img class="anchor" src="icons/tick.png" id="not_eq_true_false"theorem not_eq_true_false : a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
 @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Heq change with match a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a with [true ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a|false ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a]
 >Heq // qed.
@@ -55,6 +54,10 @@ interpretation "boolean and" 'and x y = (andb x y).
 match b1 with [ true ⇒ P b2 | false ⇒ P a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a] → P (b1 a title="boolean and" href="cic:/fakeuri.def(1)"∧/a b2).
 #b1 #b2 #P (elim b1) normalize // qed.
 
+img class="anchor" src="icons/tick.png" id="true_to_andb_true"theorem true_to_andb_true: ∀b1,b2. b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → b2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → (b1 a title="boolean and" href="cic:/fakeuri.def(1)"∧/a b2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+#b1 cases b1 normalize //
+qed.
+
 img class="anchor" src="icons/tick.png" id="andb_true_l"theorem andb_true_l: ∀ b1,b2. (b1 a title="boolean and" href="cic:/fakeuri.def(1)"∧/a b2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
 #b1 (cases b1) normalize // qed.
 
@@ -102,4 +105,4 @@ 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.
+#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.
\ No newline at end of file