Finish proofs of mwov_length, wiv_prefix, and mwov_minimal_wiv.