feat(tg-1): let-binding + de Bruijn substitution metatheory

[hyperpolymath]

Closes TG-1: type safety extended to let-binding, via the full de Bruijn substitution metatheory (the general weakening + substitution lemmas, not a closed-term shortcut).

What landed

• Syntax/typing/semantics: Expr.var (de Bruijn) + Expr.lett; tVar (context lookup Γ[i]?) + tLet; small-step letStep (congruence) + letRed (β-substitution when the bound term is a value).
• shift / subst — capture-avoiding de Bruijn operations over all ~22 Expr constructors (shift lifts free vars above a cutoff; subst substitutes-and-decrements, shifting under binders).
• weakening — HasType (Γ₁ ++ Γ₂) e τ → HasType (Γ₁ ++ σ :: Γ₂) (shift 1 Γ₁.length e) τ.
• subst_preserves — HasType (Γ₁ ++ σ :: Γ₂) e τ → HasType (Γ₁ ++ Γ₂) s σ → HasType (Γ₁ ++ Γ₂) (subst Γ₁.length s e) τ.
• Progress / Preservation / Determinism / Type Safety all extended to let; infer (+ soundness/completeness) extended, so decidability still holds.

Note on the invariant

The substitution lemma's premise is s : Γ₁ ++ Γ₂ (the combined context), not s : Γ₂ — the latter is false for a non-empty prefix (e.g. Γ₁=[α], s = var 0 would point into Γ₂ under Γ₂ but into Γ₁ under Γ₁++Γ₂). The letRed consumer instantiates Γ₁ := [], where the two coincide, so β-substitution for let v in e is subst_preserves (Γ₁:=[]) h₂ h₁.

Verification

• lean Tangle.lean → 0 errors; no sorry/axiom/admit.
• #print axioms: weakening/subst_preserves/preservation/type_safety use only propext/Quot.sound; determinism uses none. No sorryAx.

The let-free + echo-types + product/echoAdd/echoEq work is already in main (#43); this adds binders on top.

🤖 Generated with Claude Code

---

Generated by Claude Code