X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fbool_lemmas.ma;h=b03e5a62ddc181cc0378befe0728cf3cebd2f451;hb=20fdd66303330e6209059e90b6a98af71ec29567;hp=493a8e5b6524af78bf0abbfd62219340b23ac35a;hpb=661cf1186c81c15122e0644b679795d2e6b9d389;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
index 493a8e5b6..b03e5a62d 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
@@ -31,12 +31,14 @@ include "freescale/bool.ma".
 (* BOOLEANI *)
 (* ******** *)
 
-ndefinition bool_destruct :
- Πb1,b2:bool.ΠP:Prop.b1 = b2 →
+ndefinition bool_destruct_aux ≝
+Πb1,b2:bool.ΠP:Prop.b1 = b2 →
  match b1 with
   [ true ⇒ match b2 with [ true ⇒ P → P | false ⇒ P ]
   | false ⇒ match b2 with [ true ⇒ P | false ⇒ P → P ]
   ].
+
+ndefinition bool_destruct : bool_destruct_aux.
  #b1; #b2; #P;
  nelim b1;
  nelim b2;