New proof strategy for mwov2_len_calcs_nov. Improved nog_ns.
Huge renaming wave! Also introduced link between gram_normed def and fun.
Whoops, missed last rename.
Crack the induction. Progress with mwov_len_calcs_nf'.