Pterodactyl-style elaborator (problem/frame) #8

Rewrites Checker.ml as a defunctionalized stack-based elaborator. The
control flow is expressed via an explicit goal stack: G-frames drive
elaboration, K-frames consume a single produced register from the
preceding frame. Replaces the previous mutually-recursive check / infer
style on the OCaml call stack with a single dispatch loop over an ADT
of typing problems.
Architecture (see docs/superpowers/specs/2026-05-13-stack-elaborator-design.md):
- goal: 20 G/K-frame constructors covering check, infer, infer_type,
 Pi, Lambda, TypedLambda, App with implicit insertion, Hole, Max,
 lift insertion, and top-level Let / Data / Universe_decl
- machine: mutable record with goal stack, produced register, ctx,
 saved_ctx stack for binder pop/push
- dispatch: exhaustive single match; OCaml exhaustiveness gives
 compile-time coverage of all frame kinds
- Reuses Evaluation, Unification, Meta, Env, Context unchanged
Behavior parity: all 12 examples produce the same OK/FAIL outcomes
(11 OK + 1 FAIL for independent-universes-bad).
Also strips two duplicate Eio.traceln debug calls in Unification.ml
that leaked into test output.

Document Elim_def surface syntax in comment
Parse elim-header form in where-body
Align elim-keyword check with p_stack_move's match style
Expose per-ctor info lookup from ElabData
Rewrite recursive calls in clause bodies to use IH
build_elim_body driver for Elim_def Surface translation
Wire Elim_def into Checker goal machine
Rename add' to add2 in nat.vt
Drop nat.vt from parser-parity test (elim form unsupported by OldParser)
Validate clause head matches function name in elim form

Add `Inductive tag to Context.TypeContext
Move inductive ctor metadata from ElabData globals into Context tag
The inductive type's Context.S entry now carries an `Inductive ind_info tag
holding ctor list and per-ctor analysis. <= elim and <= split read it via
Context.S.resolve, so the data follows Yuujinchou's scope tree instead of
living in two flat global Hashtbls keyed by raw name.