- Remove unneeded imports
- Remove double spaces and insert space before colons
- Shorten long lines
- Favor `(.. & .. & ..)` over nesting `[.. [.. ..]]`
- Use `injection` intro patterns
- Favor `%H` over `"%H"`
- Use `first by eauto` instead of `first eauto` since the latter does not fail if `eauto` fails

- Add `Params` instance and `Proper` instances
- Use `tc_opaque` to prevent `iFrame`/`iNext` from unfolding
- Use `∗-∗` in `iff` lemma to remove `BiAffine`.

This fixes the fixme introduced in !554.
Coq issue #13654 was fixed by coq pr #14183.