Provide a better `inversion` tactic
See the discussion here:
inversion_clear often doesn't work (it produces too weak goals).
CompCert fixes the issue by providing the following tactic:
Ltac inv H := inversion H; clear H; subst.
Maybe std++ should provide a similar tactic, and replace all occurrences of
inversion_clear with that tactic. We probably want to improve some aspects:
- Include a version with an intro pattern to name the results.
- Don't just perform
subst, but only substitute the equalities generated by
Hto be an arbitrary term instead of just an