Greatly simplify induction proofs, make wiv_prefix_free beautiful.