X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcommon%2Flist_utility_lemmas.ma;h=da7c6158ef983f247bc56986c55aa3ecc33c02fa;hb=67dcf461383d4811fe2a2fb60d384804067dbc71;hp=c9d7b910fee9ad3df1197224e6062e0ffb21c552;hpb=29cfb9e2961e62c836cb50217905c0594a074e81;p=helm.git

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 c9d7b910f..da7c6158e 100755
--- 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)