freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / common / list_utility_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma
index c9d7b910fee9ad3df1197224e6062e0ffb21c552..da7c6158ef983f247bc56986c55aa3ecc33c02fa 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma
@@ -200,7 +200,7 @@ nlemma nbfoldrightlist2_to_neq
           ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize; #H3;
                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false);
                    napply (H ll2 H1 ? (list_destruct_2 T … H3));
-                   napply (or2_elim ??? (andb_false … H2) );
+                   napply (or2_elim ??? (andb_false2 … H2) );
                    ##[ ##1: #H4; napply (absurd (hh1 = hh2) …);
                             ##[ ##1: nrewrite > (list_destruct_1 T … H3); napply refl_eq
                             ##| ##2: napply (H1 … H4)
@@ -474,7 +474,7 @@ nlemma nbfoldrightnelist2_to_neq
           ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize; #H3;
                    nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false);
                    napply (H ll2 H1 ? (nelist_destruct_cons_cons_2 T … H3));
-                   napply (or2_elim ??? (andb_false … H2) );
+                   napply (or2_elim ??? (andb_false2 … H2) );
                    ##[ ##1: #H4; napply (absurd (hh1 = hh2) …);
                             ##[ ##1: nrewrite > (nelist_destruct_cons_cons_1 T … H3); napply refl_eq
                             ##| ##2: napply (H1 … H4)