Two reasons: - The equality makes it very hard to use the lemma with `rewrite`. - The version for lists `insert_zip_with` does not have the equality either.
