Freshen every distinct Typ.var in τ into its own metavariable, sharing one substitution
across all occurrences — e.g. for an .operator params ret-shaped τ, params and ret are
freshened consistently by the same substitution. Used at every Γ-reference to a scheme
binding (Elaborator/Monad.lean's Binding.isScheme, Elaborator/Expressions.lean's
inferExpr's .var case) — the checker's one instantiation point; .opCall needs no separate
specialization step since the callee's type is already specialized once looked up.
Equations
- One or more equations did not get rendered due to their size.