1) PTS simplified

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