linter.fugue.renameI #
rename_i and expose_names reach for a hypothesis by its position in the context — the one
thing every edit above them changes, silently. Name it where it is bound (rintro/obtain
pattern, case/with alternative), or with next x y => …, or do not name it at all.
Syntax quotations are exempt — split … using and injections with build rename_i into
themselves so no proof has to write it.