feat: support local hypotheses in `simp [h]` for `sym =>` mode

The `simp` tactic in `sym =>` mode now resolves identifiers in the extra
theorem list against local hypotheses first, falling back to global
constants. Local hypotheses are adapted via `mkTheoremFromExpr` (using
the `eq_true`/`eq_false`/`propext` adapter from #13041).

- Add `ExtraTheorem` inductive (`.const` / `.fvar`) for cache keying
- Add `resolveExtraTheorem` that checks the local context before globals
- Update `addExtraTheorems`, `mkDefaultMethods`, `elabVariant` signatures

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>