Maintenance.

For reasons I don't understand a proof stopped working, and removing
some rw [Once unify_def] tactics fixed it.