nnormalize;
##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
nnormalize;
##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
nnormalize;
##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
nnormalize;
##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)