linter.fugue.hypOrder

intro / rintro names should run in the order the binders appear, so a reader can match them without counting. Naming by role rather than by position (rintro ref₁ ref₃ ref₂ because ref₃ was "the aborting one") reads as a slip even when deliberate.

The linter fires only on the unambiguous case: every pattern is a plain identifier, and the names chosen are a permutation of the goal's leading binder names — the same names, reordered. Fresh names that do not match the binders are a free rename and are left alone; a deliberate reorder takes the per-site escape.