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 bc146e793f2b0fb8d2b1df262b13018a464e0c67..7d60068626139b3d103f667e4586911c3364d5b2 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,12 +40,14 @@ ndefinition bool_destruct : bool_destruct_aux.
  nelim b2;
  nnormalize;
  #H;
- ##[ ##2: napply (False_ind ??);
+ ##[ ##2: napply (False_ind (λx.P) ?);
+          (* perche' non napply (False_ind ??); !!! *)
           nchange with (match true with [ true ⇒ False | false ⇒ True]);
           nrewrite > H;
           nnormalize;
           napply I
- ##| ##3: napply (False_ind ??);
+ ##| ##3: napply (False_ind (λx.P) ?);
+          (* perche' non napply (False_ind ??); !!! *)
           nchange with (match true with [ true ⇒ False | false ⇒ True]);
           nrewrite < H;
           nnormalize;
@@ -104,7 +106,7 @@ nlemma symmetric_xorbool : symmetricT bool bool xor_bool.
  napply (refl_eq ??).
 nqed.
 
-nlemma associative_orbool : ∀b1,b2,b3.((b1 ⊙ b2) ⊙ b3) = (b1 ⊙ (b2 ⊙ b3)).
+nlemma associative_xorbool : ∀b1,b2,b3.((b1 ⊙ b2) ⊙ b3) = (b1 ⊙ (b2 ⊙ b3)).
  #b1; #b2; #b3;
  nelim b1;
  nelim b2;