##| ##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)
##| ##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)