refactor: migrate to the new do elaborator

[kim-em]

Stacked on digama0#30.

Resolves digama0#31.

Summary

• remove the four backward.do.legacy compatibility pins
• migrate the verifier proofs to the new do elaborator
• make the experimental shape lifts use explicit Option.bind terms with result type ascriptions

Verification

• lake build
• lake build Lean4Lean.Experimental
• lake exe lean4lean Init.Core
• lake exe lean4lean --fresh Init.System.IO

Coverage note

Removing the TypeChecker.lean pin changes elaborated terms in code paths whose existing .WF theorems still contain sorry (reduceRecursor, reduceProj, inferProj, tryEtaStructCore, and isDefEqUnitLike). The fresh Init.System.IO replay is therefore part of the safety check, rather than relying only on proof coverage.

Independent review

A fresh Claude Opus review found no correctness regression and confirmed that the explicit Option.bind rewrites preserve behavior. Follow-up changes narrowed both new simp attributes, replaced a broad Expr constructor case split with targeted Boolean elimination, made the experimental proof branches explicit, and cleaned stale join-point names.

[kim-em]

Superseded by the correctly placed upstream draft: digama0#33.