freescale porting, work in progress

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

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 87a166d174de033e6d9806077f323830e551481b..a837712532b655071995e3f24133e367f9432a67 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
@@ -41,13 +41,11 @@ ndefinition bool_destruct : bool_destruct_aux.
  nnormalize;
  #H;
  ##[ ##2: napply (False_ind (λx.?) ?);
-          (* perche' non napply (False_ind ??); !!! *)
           nchange with (match true with [ true ⇒ False | false ⇒ True]);
           nrewrite > H;
           nnormalize;
           napply I
  ##| ##3: napply (False_ind (λx.?) ?);
-          (* perche' non napply (False_ind ??); !!! *)
           nchange with (match true with [ true ⇒ False | false ⇒ True]);
           nrewrite < H;
           nnormalize;