freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / num / bool_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma
index b7b9096e871706bddcb98a46ce4b85db2221168c..fddf6d832e44db0db7057e39d002b4fa171cdc8a 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma
@@ -26,7 +26,7 @@ include "num/bool.ma".
 (* BOOLEANI *)
 (* ******** *)
 
-ndefinition bool_destruct_aux ≝
+(*ndefinition bool_destruct_aux ≝
 Πb1,b2:bool.ΠP:Prop.b1 = b2 →
  match eq_bool b1 b2 with [ true ⇒ P → P | false ⇒ P ].
 
@@ -36,7 +36,7 @@ ndefinition bool_destruct : bool_destruct_aux.
  nelim b1;
  nnormalize;
  napply (λx.x).
-nqed.
+nqed.*)
 
 nlemma symmetric_eqbool : symmetricT bool bool eq_bool.
  #b1; #b2;
@@ -103,7 +103,7 @@ nlemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2).
  ncases b2;
  nnormalize;
  ##[ ##1,4: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
  ##]
 nqed.