translateTerm refactoring and proof coverage

[tautschnig]

While reading #1107 the following was noticed:

Refactoring opportunities (out of scope, but worth a follow-up). translateTerm is ~320 lines of nearly-repeated match arms grouped by a few shapes:

• bitvec unary op → (mkBitVec w, .app (mkThing w) x)
• bitvec binary comparison → (mkProp, mkBoolToProp ...)
• bitvec binary arithmetic → (mkBitVec w, ...)
• int binary comparison → (mkProp, mkApp2 mkIntXX x y)
• int binary arithmetic → leftAssocOp mkIntXX

Extracting small helpers for each shape would both shrink the function and remove the opportunity for precisely this kind of typo (the single point where the Lean type is produced is reviewed once, not 20+ times). A stronger-typed return modelled on Denote.lean's TermDenoteResult — where the reflected Lean Type is part of the result and a wrong annotation is a type error rather than a logic error — would subsume the need for per-case care entirely. Either is a reasonable follow-up; not blocking.

Proof-coverage suggestion. A natural target invariant — even if stated only as a property-based test via plausible over a generator of SMT.Term — is:

For every well-typed t : SMT.Term, (translateTerm t).run' {} = .ok (α, e) implies α = translateSort (typeOf t) and e type-checks against α in Lean's kernel.

Since translateTerm is MetaM-shaped code producing Lean.Expr, an object-level theorem is awkward, but the first conjunct (α = translateSort (typeOf t)) is decidable and a small generator-driven check would mechanically cover the whole match in one shot. The TermDenoteResult-style refactor mentioned above would of course make this an internal theorem of the definition rather than an external test.