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