insert_leaf_split_never_empty changed to use destruct instead of inversion, as it never used the IH.