diff --git a/docs/NovaElaboration.txt b/docs/NovaElaboration.txt
index 4951a32..342e92a 100644
--- a/docs/NovaElaboration.txt
+++ b/docs/NovaElaboration.txt
@@ -145,6 +145,10 @@ T{0} ::= t{≥2} ≡ t{≥2} ∈ T{≥1}
 t{5} ::= x | () | Z | ⋆ | ∥T{≥0}∥ | 𝟘 | 𝟙 | ℕ | (t{≥0}) | (t{≥0} : T{≥0})
 t{3} ::= t{≥3} t{≥4} | t{≥3} .π₁ | t{≥3} .π₂                 (left-assoc)
 t{2} ::= λx. t{≥1½}
+       | let x ≔ t{≥0} in t{≥1½}                              # let-expression
+       | let x : T{≥0} ≔ t{≥0} in t{≥1½}                      #   (annotated
+                                                              #   definiens) —
+                                                              #   see e-let
        | 𝟘-elim t{≥4}
        | S t{≥4}
        | ℕ-elim (n. T{≥0}) t{≥4} (n ih. t{≥4}) t{≥4}          # motive, z, s, scrutinee
@@ -306,7 +310,8 @@ instead an error asking the user for an ascription or annotation.
 //////// whnf ////////
 
 whnf(–) is weak-head normalization by Foundation's ≜ rules:
-el-pi-beta, el-sigma-beta₁, el-sigma-beta₂, el-nat-beta-z,
+el-pi-beta, el-let-beta (a let is always a redex — no whnf ever
+returns one), el-sigma-beta₁, el-sigma-beta₂, el-nat-beta-z,
 el-nat-beta-s, el-sum-beta₁, el-sum-beta₂, el-quot-beta,
 el-nu-beta (out at a corec head — map_𝔽 and hᵉˡ expanding by
 Foundation's ≜-clauses), el-qiit-beta (the eliminator at a
@@ -428,6 +433,21 @@ componentwise at F ⨯ G and F ⊎ G                  (e-poly-prod, e-poly-sum)
 ---------------------- (e-ann)
 Γ ⊢ (t : T) ⇒ A ⇝ t̂
 
+Γ ⊢ e ⇒ A ⇝ ê
+Γ ▷ x:A ▷ h:Prf (☐₀ ≡ ê[↑] ∈ A[↑]) ⊢ b ⇒ B ⇝ b̂
+-------------------------------------------------- (e-let)    # (let a b)
+Γ ⊢ let x ≔ e in b ⇒ B[id, ê, ⋆] ⇝ let ê b̂
+# The DEFINIENS is inferred — a checking-only definiens (λ, pair, ...)
+# takes the annotated form, which is parse-level sugar for ascription:
+#     let x : T ≔ e in b   ≜   let x ≔ (e : T) in b
+# The BODY is elaborated under x AND the unfolding hypothesis h. h's
+# type is a Prf of an equality prop, so E's HYPOTHESIS source reflects
+# ☐₁ ≐ ê[↑ ∘ ↑] into discharge automatically: the definition is
+# TRANSPARENT inside the body with no new mechanism — Foundation's
+# el-let, the definition-carrying-context reading. h never appears in
+# b (nothing binds it on the surface); it exists for discharge and for
+# the kernel's context, and the report printer renders it silently.
+
 Γ ▷ n:ℕ ⊢ T ⇝ A type
 Γ ⊢ z ⇐ A[id, Z] ⇝ ẑ
 Γ ▷ n:ℕ ▷ ih:A ⊢ s ⇐ A[↑ ∘ ↑, S ☐₁] ⇝ ŝ
@@ -692,6 +712,17 @@ whnf(C) = Prf ∥A∥        Γ ⊢ e ⇐ A ⇝ ê
 # Any expected C; 𝟘-elim is the one form that checks against
 # everything. In inference position it is a structural error (ascribe).
 
+Γ ⊢ e ⇒ A ⇝ ê
+Γ ▷ x:A ▷ h:Prf (☐₀ ≡ ê[↑] ∈ A[↑]) ⊢ b ⇐ C[↑ ∘ ↑] ⇝ b̂
+--------------------------------------------------------- (e-let-check)
+Γ ⊢ let x ≔ e in b ⇐ C ⇝ let ê b̂
+# let PROPAGATES the ambient mode to its body — this direct checking
+# rule (rather than e-let + e-switch) is what lets a checking-only
+# body form (a λ, a pair, a ⋆) sit under a let without ascription.
+# C lives over Γ, so checking b at C[↑ ∘ ↑] is fully general, not an
+# approximation (docs/NovaKernel.txt §8, el-let). The definiens and
+# the hypothesis are exactly as at e-let.
+
 Γ ⊢ t ⇒ B ⇝ t̂        Γ ⊢ B ≐ C type ↓
 --------------------------------------- (e-switch)
 Γ ⊢ t ⇐ C ⇝ t̂
@@ -705,7 +736,9 @@ whnf(C) = Prf ∥A∥        Γ ⊢ e ⇐ A ⇝ ê
 # squash-elim, 𝟘-elim (their types are not determined by their syntax
 # — an injection alone does not determine the OTHER summand);
 # encountering one in inference position is a structural error whose
-# fix is an ascription. Everything else — including ∥-∥ — infers and
+# fix is an ascription. let is BOTH-MODE: its body elaborates in the
+# ambient mode (e-let / e-let-check), its definiens always in
+# inference mode. Everything else — including ∥-∥ — infers and
 # reaches checking mode through e-switch.
 
 //////////// Conversion and discharge (the ↓ judgements) /////////////
diff --git a/docs/NovaFoundation.txt b/docs/NovaFoundation.txt
index 806a8ab..11282ec 100644
--- a/docs/NovaFoundation.txt
+++ b/docs/NovaFoundation.txt
@@ -1,6 +1,6 @@
 ////////// Preface //////////
 
-#! highlight keywords: ⊦ : ; , · [ ] ‖ .π₁ .π₂ ∈ ∋ ≐ ≜ ≔ ⇒ ⇐ = ⬡ ⬦ ▷ ◁ ⇛ ⇑ 𝕚𝕕 El U ☐ ε ↑ ∘ ⁺ id λ → ⨯ ⊎ ≡ ∥ / Ω 𝕌 ℕ 𝟘 𝟙 Z S ⋆ Prf class inj₁ inj₂ ⌊ ⌋ ⟦ ⟧ ⋈ ⋉ ᴰ 𝟘-elim ℕ-elim quot-elim squash-elim ⊎-elim -elim qctx qty qsig ctx type tel mot dalg eprob sect norm small sig nf qpath ν 𝕏 K out corec poly map
+#! highlight keywords: ⊦ : ; , · [ ] ‖ .π₁ .π₂ ∈ ∋ ≐ ≜ ≔ ⇒ ⇐ = ⬡ ⬦ ▷ ◁ ⇛ ⇑ 𝕚𝕕 El U ☐ ε ↑ ∘ ⁺ id λ let → ⨯ ⊎ ≡ ∥ / Ω 𝕌 ℕ 𝟘 𝟙 Z S ⋆ Prf class inj₁ inj₂ ⌊ ⌋ ⟦ ⟧ ⋈ ⋉ ᴰ 𝟘-elim ℕ-elim quot-elim squash-elim ⊎-elim -elim qctx qty qsig ctx type tel mot dalg eprob sect norm small sig nf qpath ν 𝕏 K out corec poly map
 #! highlight tos: 𝔄 𝔅 𝕥 𝕦 𝕧 𝕤 𝕔 𝕜 𝕘 𝕒 𝕓 𝕞 Φ 𝒮 ς 𝔎 𝔽 𝔾
 #! highlight nova: Γ Δ Ξ Σ σ τ δ θ latin
 #! highlight meta: 𝑤 ρ υ π 𝒞 ℰ
@@ -146,6 +146,9 @@ t ::= x [e˲]         # element in the signature context
     | ☐ᵢ             # i-th element in the typing context
     | λ t            # dependent product type introduction
     | t t            # dependent product type elimination
+    | let t t        # let-expression (definiens, body — the body
+                     #   binds the definiens AND its unfolding
+                     #   equation; see the let block)
     | t , t          # dependent sum type introduction
     | t .π₁          # dependent sum type elimination (1)
     | t .π₂          # dependent sum type elimination (2)
@@ -1064,6 +1067,36 @@ e˲ : Γ₁ ⇒ Γ norm
 --------------------------------- (el-pi-eta)
 Γ ⊦ λ (f[↑] ☐₀) ≐ f : A → B
 
+# let — the local DEFINITION: the body is typed under TWO binders,
+# the definiens' value and its UNFOLDING EQUATION, so inside b the
+# definiendum unfolds judgementally — el-reflect on ☐₀ gives
+# ☐₁ ≐ a[↑ ∘ ↑] : A[↑ ∘ ↑]. This is a definition-carrying context
+# discipline (Γ ▷ (x ≔ a : A)) with NO new context former:
+# extensionally a definition IS a variable plus a Prf of its
+# unfolding — the same degeneration that collapses the QIIT
+# coherence tower. el-let-beta unfolds the whole expression to the
+# instantiated body, the ⋆ typed by el-eq-i at the reflexive
+# instance a ≡ a, so a let and its unfolding are interchangeable
+# everywhere. NOT a type former — nothing is introduced or
+# eliminated, hence no eta and no injectivity — and DEFINABLE:
+# let a b ≐ ((λ (λ b)) a) ⋆ (two el-pi-beta steps compute the
+# encoding to b[id, a, ⋆]; ty-pi forms its Π-types from the
+# premises' presuppositions). Retained like ℕ and (/) for
+# convenience, not necessity — here the convenience is SYNTACTIC
+# IDENTITY: a local definition should read (and print) as one, not
+# as its λ-plumbing. A body that ignores the equation just weakens
+# past ☐₀ — the "weak" (opaque-binder) let is the special case.
+
+Γ ⊦ a : A
+Γ ▷ A ▷ Prf (☐₀ ≡ a[↑] ∈ A[↑]) ⊦ b : B
+------------------------------------------ (el-let)
+Γ ⊦ let a b : B[id, a, ⋆]
+
+Γ ⊦ a : A
+Γ ▷ A ▷ Prf (☐₀ ≡ a[↑] ∈ A[↑]) ⊦ b : B
+---------------------------------------------- (el-let-beta)
+Γ ⊦ let a b ≜ b[id, a, ⋆] : B[id, a, ⋆]
+
 # Σ.
 
 Γ ▷ A ⊦ B type
@@ -2139,6 +2172,15 @@ e˲ : Δ ⇒ Γ norm
 ------------------------------------------ (el-sub-app)
 Γ₀ ⊦ (f e)[σ] ≜ f[σ] e[σ] : B[σ, e[σ]]
 
+Γ₁ ⊦ a : A
+Γ₁ ▷ A ▷ Prf (☐₀ ≡ a[↑] ∈ A[↑]) ⊦ b : B
+σ : Γ₀ ⇒ Γ₁
+------------------------------------------------------- (el-sub-let)
+Γ₀ ⊦ (let a b)[σ] ≜ let a[σ] b[σ⁺⁺] : B[σ, a[σ], ⋆]
+# (coherent: ☐₀[σ⁺] ≜ ☐₀ and a[↑][σ⁺] ≐ a[σ][↑], so the Prf entry
+# lands as the unfolding equation OF a[σ] — the RHS is the let at
+# a[σ] — and ⋆[σ] ≜ ⋆ keeps the conclusion type in shape)
+
 Γ₁ ▷ A ⊦ B type
 Γ₁ ⊦ a : A
 Γ₁ ⊦ b : B[id, a]
@@ -2291,6 +2333,14 @@ e˲ : Γ₁ ⇒ Γ norm
 ------------------------------------ (el-app-cong)
 Γ ⊦ f₀ a₀ ≐ f₁ a₁ : B[id, a₁]
 
+Γ ⊦ a₀ ≐ a₁ : A
+Γ ▷ A ▷ Prf (☐₀ ≡ a₁[↑] ∈ A[↑]) ⊦ b₀ ≐ b₁ : B
+--------------------------------------------------- (el-let-cong)
+Γ ⊦ let a₀ b₀ ≐ let a₁ b₁ : B[id, a₁, ⋆]
+# (the a₀- and a₁-instance contexts are equal — ctx-ext-cong with
+# code-eq-cong — so the premise is stated at the a₁ instance, as at
+# the other congruences)
+
 Γ ▷ A ⊦ B type
 Γ ⊦ a₀ ≐ a₁ : A
 Γ ⊦ b₀ ≐ b₁ : B[id, a₁]
diff --git a/docs/NovaKernel.txt b/docs/NovaKernel.txt
index d6d7411..e762771 100644
--- a/docs/NovaKernel.txt
+++ b/docs/NovaKernel.txt
@@ -49,6 +49,9 @@ are not listed; the contraction clauses, each of which burns one unit
 of fuel, are exactly:
 
   (λ f) e            ≜  f[id, e]                    # el-pi-beta
+  let a b            ≜  b[id, a, ⋆]                 # el-let-beta (a let is
+                                                    # ALWAYS a redex: normal
+                                                    # forms contain no let)
   (a , b) .π₁        ≜  a                           # el-sigma-beta₁
   (a , b) .π₂        ≜  b                           # el-sigma-beta₂
   ℕ-elim z s Z       ≜  z                           # el-nat-beta-z
@@ -201,6 +204,7 @@ Child indexing, shared by paths, the typed descent (§6) and skeletons
   elements:  𝟘-elim t → 0            S t → 0
              ℕ-elim z s t → 0, 1(2), 2
              λ f → 0(1)              f e → 0, 1
+             let a b → 0, 1(2)       # body under value + unfolding-Prf binders
              (a , b) → 0, 1          t.π₁ / t.π₂ → 0
              inj₁ t / inj₂ t → 0     ⊎-elim l r t → 0(1), 1(1), 2
              a →ᶜ b → 0, 1(1)        a ⨯ᶜ b → 0, 1(1)
@@ -327,6 +331,12 @@ introduction forms structurally and falls back to infer-and-compare:
 Signature substitutions e˲ ⇐ᵖ Δ are checked entrywise, entry i's
 telescope type instantiated by the preceding entries (sub-norm-ext).
 
+let-expressions are NOT in the proof fragment (neither ⇒ᵖ nor ⇐ᵖ):
+a license containing one is rejected. Nothing is lost — a let is
+always a redex (§1), so the elaborator emits licenses let-free;
+a lemma whose body wants one is referenced through Σ, where the
+item level checks lets directly (§8).
+
 ////////// 4. What a step licenses //////////
 
 A step (onLhs, path, lic, sels, flip) licenses one equation, derived —
@@ -433,6 +443,9 @@ type E; — means undetermined):
                   child 1 : E[↑][↑]      # ditto
                   child 2 : ℕ
   λ f             child 0 : B            when nf(E) ⇓ A → B
+  let a b         (never reached: replay normalizes both sides before
+                   any step (§7) and a let is always a redex (§1), so
+                   no rewrite path meets one)
   f e             child 0 : —
                   child 1 : A            when f is an inferable spine
                                          # ⇒ᴺ, below
@@ -600,6 +613,17 @@ Checking  Σ; Γ ⊦ t ⇐ T ⟨sk⟩ :
      -----------------------------------------          # el-pi-i
      Σ; Γ ⊦ λ f ⇐ T ⟨sk⟩
 
+     Σ; Γ ⊦ a ⇒ A ⟨sk.0⟩
+     Σ; Γ ▷ A ▷ Prf (☐₀ ≡ a[↑] ∈ A[↑]) ⊦ b ⇐ T[↑ ∘ ↑] ⟨sk.1⟩
+     --------------------------------------------------------
+     Σ; Γ ⊦ let a b ⇐ T ⟨sk⟩                            # el-let
+     # T lives over Γ, so checking b at T[↑ ∘ ↑] is fully general,
+     # not an approximation: under the unfolding hypothesis
+     # (id, a, ⋆) ∘ (↑ ∘ ↑) ≐ id (el-reflect on ☐₀ plus el-prf-prop),
+     # so any valid body type is ≐ T[↑ ∘ ↑]. The definiens is
+     # INFERRED — an intro-form definiens carries intro-ty on sk.0,
+     # the ascription route.
+
      nf(T) ⇓ A ⨯ B    Σ; Γ ⊦ u ⇐ A ⟨sk.0⟩   Σ; Γ ⊦ v ⇐ B[id,u] ⟨sk.1⟩
      ---------------------------------------------------------------
      Σ; Γ ⊦ (u , v) ⇐ T ⟨sk⟩                            # el-sigma-i
@@ -684,6 +708,13 @@ Inference  Σ; Γ ⊦ t ⇒ T ⟨sk⟩ :
 
      (projections analogously: el-sigma-e₁/₂)
 
+  let infers when its body does (definiens inferred, as in checking):
+
+     Σ; Γ ⊦ a ⇒ A ⟨sk.0⟩
+     Σ; Γ ▷ A ▷ Prf (☐₀ ≡ a[↑] ∈ A[↑]) ⊦ b ⇒ B ⟨sk.1⟩
+     ------------------------------------------------------------
+     Σ; Γ ⊦ let a b ⇒ B[id, a, ⋆]                       # el-let
+
   ℕ-elim demands its motive — the REAL rule, no approximation here:
 
      sk carries motive M ⟨skM⟩       Σ; Γ ▷ ℕ ⊦ M type ⟨skM⟩
diff --git a/src/idris/Nova/Compute.idr b/src/idris/Nova/Compute.idr
index c5d34e0..9cf3042 100644
--- a/src/idris/Nova/Compute.idr
+++ b/src/idris/Nova/Compute.idr
@@ -129,6 +129,8 @@ mutual
     case whnfElem sig f of
       PiIntro g => whnfElem sig (substElem g (Ext Id e))
       _ => assert_total $ idris_crash "whnfElem: application head is not a function (impossible for a closed, well-typed term)"
+  -- el-let-beta: a let is ALWAYS a redex
+  whnfElem sig (Let a b) = whnfElem sig (substElem b (Ext (Ext Id a) Star))
   whnfElem sig (SigmaIntro a b)   = SigmaIntro a b
   whnfElem sig (SigmaElim1 t) =
     case whnfElem sig t of
@@ -255,6 +257,7 @@ mutual
     go (Elem.EqTy l r t)  = Elem.EqTy (nfElem sig l) (nfElem sig r) (nfTy sig t)
     go (QuotTy a r)       = QuotTy (nfElem sig a) r   -- r: under a binder, left alone
     go (SigVar x es)      = SigVar x es   -- unreachable: whnf always unfolds x[e˲]
+    go (Let a b)          = Let a b   -- unreachable: whnf always contracts a let
     go (Class a)          = Class (nfElem sig a)
     go (QuotElim f q)     = QuotElim f (nfElem sig q)   -- f: under a binder, left alone
     go (Squash t)         =
diff --git a/src/idris/Nova/Elaboration.idr b/src/idris/Nova/Elaboration.idr
index 13ce2fa..245b53b 100644
--- a/src/idris/Nova/Elaboration.idr
+++ b/src/idris/Nova/Elaboration.idr
@@ -251,6 +251,7 @@ mapRefsE f (NatIntro1 t) = NatIntro1 (mapRefsE f t)
 mapRefsE f (NatElim z s t) = NatElim (mapRefsE f z) (mapRefsE f s) (mapRefsE f t)
 mapRefsE f (PiIntro g) = PiIntro (mapRefsE f g)
 mapRefsE f (PiApp g e) = PiApp (mapRefsE f g) (mapRefsE f e)
+mapRefsE f (Let a b) = Let (mapRefsE f a) (mapRefsE f b)
 mapRefsE f (SigmaIntro a b) = SigmaIntro (mapRefsE f a) (mapRefsE f b)
 mapRefsE f (SigmaElim1 t) = SigmaElim1 (mapRefsE f t)
 mapRefsE f (SigmaElim2 t) = SigmaElim2 (mapRefsE f t)
@@ -333,6 +334,7 @@ collectRefsE e = go e
   go (NatElim z s t) = go z ++ go s ++ go t
   go (PiIntro f) = go f
   go (PiApp f x) = go f ++ go x
+  go (Let a b) = go a ++ go b
   go (SigmaIntro a b) = go a ++ go b
   go (SigmaElim1 t) = go t
   go (SigmaElim2 t) = go t
@@ -737,6 +739,7 @@ elemSize (NatIntro1 t) = S (elemSize t)
 elemSize (NatElim z s t) = S (elemSize z + elemSize s + elemSize t)
 elemSize (PiIntro f) = S (elemSize f)
 elemSize (PiApp f e) = S (elemSize f + elemSize e)
+elemSize (Let a b) = S (elemSize a + elemSize b)
 elemSize (SigmaIntro u v) = S (elemSize u + elemSize v)
 elemSize (SigmaElim1 t) = S (elemSize t)
 elemSize (SigmaElim2 t) = S (elemSize t)
@@ -1818,6 +1821,8 @@ mutual
     case zonkElem st f of
       PiIntro g => zonkElem st (substElem g (Ext Id e))
       f2 => PiApp f2 (zonkElem st e)
+  -- el-let-beta: a let is always a redex
+  zonkElem st (Let a b) = zonkElem st (substElem b (Ext (Ext Id a) Star))
   zonkElem st (SigmaIntro a b) = SigmaIntro (zonkElem st a) (zonkElem st b)
   zonkElem st (SigmaElim1 t) =
     case zonkElem st t of
@@ -3008,6 +3013,17 @@ mutual
     (ty', tySk) <- elabTy ctx env site ty
     (t', tSk) <- checkElem ctx env site t ty'
     pure (t', ty', addPayload (PIntroTy ty' tySk) tSk)
+  inferElem ctx env site (SLet (x, xr) e b) = do
+    -- e-let: the definiens is INFERRED (an annotated surface let
+    -- arrives as an ascribed definiens); the body is elaborated under
+    -- the value AND its unfolding hypothesis — a Prf of an equality
+    -- prop, so E's HYPOTHESIS source reflects x ≐ e into discharge
+    -- automatically: the definition is transparent inside the body
+    (e', eTy, eSk) <- inferElem ctx env site e
+    recordBinder xr ctx env x eTy
+    let hyp = Prf (Elem.EqTy (CtxVar 0) (substElem e' Wk) (substTy eTy Wk))
+    (b', bTy, bSk) <- inferElem (ctx :< eTy :< hyp) (env :< x :< wildcard) site b
+    pure (Let e' b', substTy bTy (Ext (Ext Id e') Star), Nd [] [eSk, bSk])
   inferElem ctx env site (SNatElim (n, nr) mot z (n2, n2r) (ih, ihr) s t) = do
     recordBinder nr ctx env n Ty.NatTy
     (motTy, motSk) <- elabTy (ctx :< Ty.NatTy) (env :< n) site mot
@@ -3355,6 +3371,18 @@ mutual
         modifySt $ { sig $= (:< SigDecl ctx q ty)
                    , holeMeta $= (:< MkHoleMeta q env site solvable mrng) }
         pure (SigVar q (idSpine (length ctx)), baseSk)
+  checkElem ctx env site (SLet (x, xr) e b) ty = do
+    -- e-let-check: let PROPAGATES the ambient mode to its body (a
+    -- checking-only body form works under a let without ascription).
+    -- The expected type lives over Γ, so the body checks at its double
+    -- weakening — fully general, not an approximation (docs/
+    -- NovaKernel.txt §8, el-let)
+    (e', eTy, eSk) <- inferElem ctx env site e
+    recordBinder xr ctx env x eTy
+    let hyp = Prf (Elem.EqTy (CtxVar 0) (substElem e' Wk) (substTy eTy Wk))
+    (b', bSk) <- checkElem (ctx :< eTy :< hyp) (env :< x :< wildcard) site b
+                   (substTy (substTy ty Wk) Wk)
+    pure (Let e' b', Nd [] [eSk, bSk])
   checkElem ctx env site t ty = do
     (t', inferred, tSk) <- inferElem ctx env site t
     c <- convTy ctx env "\{site}: inferred vs expected type" Nothing inferred ty
diff --git a/src/idris/Nova/Elaboration/Named.idr b/src/idris/Nova/Elaboration/Named.idr
index 9b32da1..0eb2e58 100644
--- a/src/idris/Nova/Elaboration/Named.idr
+++ b/src/idris/Nova/Elaboration/Named.idr
@@ -241,6 +241,7 @@ mutual
   usesIndexElem k (NatElim z s t) = usesIndexElem k z || usesIndexElem (S (S k)) s || usesIndexElem k t
   usesIndexElem k (PiIntro e) = usesIndexElem (S k) e
   usesIndexElem k (PiApp f e) = usesIndexElem k f || usesIndexElem k e
+  usesIndexElem k (Let a b) = usesIndexElem k a || usesIndexElem (S (S k)) b
   usesIndexElem k (SigmaIntro e e') = usesIndexElem k e || usesIndexElem k e'
   usesIndexElem k (SigmaElim1 e) = usesIndexElem k e
   usesIndexElem k (SigmaElim2 e) = usesIndexElem k e
@@ -363,6 +364,15 @@ mutual
   prettyElemPrefixN tbl env (PiIntro e) =
     let x = freshGeneric env
     in "λ" ++ x ++ ". " ++ prettyElemOpN tbl (env :< x) 0 e
+  prettyElemPrefixN tbl env (Let a b) =
+    -- surface-faithful: the unfolding-equation binder has no surface
+    -- spelling and elaborator-produced bodies never reference it; it
+    -- still enters the env (under a fresh Prf-flavored name) so a
+    -- reference in hand-built core would at least print visibly
+    let x = freshGeneric env
+        h = freshFromList candidatesPrf (env :< x)
+    in "let " ++ x ++ " ≔ " ++ prettyElemN tbl env a ++ " in "
+         ++ prettyElemOpN tbl (env :< x :< h) 0 b
   prettyElemPrefixN tbl env (ZeroElim e) = "𝟘-elim " ++ prettyElemAtomN tbl env e
   prettyElemPrefixN tbl env (NatIntro1 e) = "S " ++ prettyElemAtomN tbl env e
   prettyElemPrefixN tbl env (NatElim z s t) =
diff --git a/src/idris/Nova/Elaboration/Parser.idr b/src/idris/Nova/Elaboration/Parser.idr
index cef1ecb..0eab9f3 100644
--- a/src/idris/Nova/Elaboration/Parser.idr
+++ b/src/idris/Nova/Elaboration/Parser.idr
@@ -107,10 +107,13 @@ parseName = do
     -- so the parse fails deep and confusingly) or silently for Z/Refl
     -- (bare tokens — a reference just parses as the literal zero/Refl,
     -- no error at all).
+    -- let/in are reserved for the same reason as S/class: both are
+    -- syntactically valid identifiers, and a binder named `in` would
+    -- misparse every let-body boundary after it
     guard "Reserved keyword" (name /= "def" && name /= "type" && name /= "El" && name /= "Prf" &&
                               name /= "import" && name /= "infixl" && name /= "infixr" &&
                               name /= "S" && name /= "Z" && name /= "class" &&
-                              name /= "data")
+                              name /= "data" && name /= "let" && name /= "in")
     pure name
 
 ||| A name with its span — binder positions record it so the LSP can
@@ -346,6 +349,21 @@ mutual
         -- λ's body extends over operators: λx. x + y ≡ λx. (x + y)
         (do kw "λ"; sp; x <- parseNameR; sp; kwc '.'; sp
             e <- parseSElemOp tbl (env :< fst x); pure (SLam x e))
+        -- let x ≔ e in b / let x : T ≔ e in b — the annotated form is
+        -- sugar for an ascribed definiens (the definiens elaborates in
+        -- inference mode); the body extends over operators, like λ's.
+        -- The body's indices are counted against the CORE context,
+        -- which has TWO entries per let (el-let: the value, then its
+        -- unfolding equation) — so x is pushed under a wildcard slot
+        -- and resolves to index 1, the hypothesis slot (never
+        -- resolvable) holding index 0
+    <|> (do kw "let"; space; x <- parseNameR; sp
+            manno <- optional (do kwc ':'; sp; t <- parseSTy tbl env; sp; pure t)
+            kw "≔"; sp
+            e <- parseSElem tbl env; sp
+            kw "in"; sp
+            b <- parseSElemOp tbl (env :< fst x :< wildcard)
+            pure (SLet x (maybe e (SAnn e) manno) b))
     <|> (do kw "𝟘-elim"; space; e <- parseSElemAtom tbl env; pure (SZeroElim e))
     <|> (do kw "ℕ-elim"; space
             kwc '('; sp; n <- parseNameR; sp; kwc '.'; sp
diff --git a/src/idris/Nova/Elaboration/Surface.idr b/src/idris/Nova/Elaboration/Surface.idr
index a487c5f..322d930 100644
--- a/src/idris/Nova/Elaboration/Surface.idr
+++ b/src/idris/Nova/Elaboration/Surface.idr
@@ -86,6 +86,12 @@ mutual
     SSuc : SElem -> SElem
     ||| λx. t
     SLam : (name : SName) -> SElem -> SElem
+    ||| let x ≔ e in b — the body binds x (the definiens' value); the
+    ||| unfolding-equation binder of the core form (el-let) is inserted
+    ||| by elaboration and has no surface spelling. An annotated
+    ||| definiens (let x : T ≔ e in b) is parse-level sugar for
+    ||| let x ≔ (e : T) in b.
+    SLet : (name : SName) -> SElem -> SElem -> SElem
     SApp : SElem -> SElem -> SElem
     SPair : SElem -> SElem -> SElem
     SProj1 : SElem -> SElem
@@ -291,6 +297,7 @@ mutual
     show SZeroN = "Z"
     show (SSuc t) = "S (\{show t})"
     show (SLam x t) = "Lam \{fst x} (\{show t})"
+    show (SLet x e b) = "Let \{fst x} (\{show e}) (\{show b})"
     show (SApp f e) = "App (\{show f}) (\{show e})"
     show (SPair a b) = "Pair (\{show a}) (\{show b})"
     show (SProj1 t) = "P1 (\{show t})"
diff --git a/src/idris/Nova/Kernel.idr b/src/idris/Nova/Kernel.idr
index 78c7e2a..4e30b4a 100644
--- a/src/idris/Nova/Kernel.idr
+++ b/src/idris/Nova/Kernel.idr
@@ -236,6 +236,11 @@ mutual
     case f' of
       PiIntro g => do burn; kElem sig (substElem g (Ext Id e'))
       _ => pure (PiApp f' e')
+  -- el-let-beta: a let is ALWAYS a redex — let a b ≜ b[id, a, ⋆]
+  -- (normal forms contain no let; one fuel unit, like every contraction)
+  kElem sig (Let a b) = do
+    burn
+    kElem sig (substElem b (Ext (Ext Id a) Star))
   kElem sig (SigmaIntro a b) = [| SigmaIntro (kElem sig a) (kElem sig b) |]
   kElem sig (SigmaElim1 t) = do
     t' <- kElem sig t
@@ -1741,6 +1746,15 @@ mutual
                 kCheckE sig ctx x (El aC) (skelChild 2 sk)
               _ => kerr "kernel: corec checked at a non-ν type"
           ZeroElim t => kCheckE sig ctx t Ty.ZeroTy (skelChild 0 sk)
+          -- el-let (spec §8): definiens INFERRED (an intro-form
+          -- definiens carries intro-ty on child 0), body under the
+          -- value and its unfolding equation, checked at T[↑ ∘ ↑] —
+          -- fully general, since T lives over Γ and the hypothesis
+          -- makes (id, a, ⋆) ∘ (↑ ∘ ↑) ≐ id
+          Let a b => do
+            aTy <- kInferE sig ctx a (skelChild 0 sk)
+            let hyp = Prf (Elem.EqTy (CtxVar 0) (substElem a Wk) (substTy aTy Wk))
+            kCheckE sig (ctx :< aTy :< hyp) b (weakenTyN 2 ty) (skelChild 1 sk)
           QCtor sgC c theta => do
             -- el-qiit-intro, SATURATED. The signature is nf(T)'s own —
             -- already validated where T was — and the term's must be
@@ -1840,6 +1854,13 @@ mutual
             case tTy of
               Ty.NuTy f => pure (El (reflectPoly f (Elem.NuTy f)))
               _ => kerr "kernel: observing a non-ν element"
+          -- el-let (spec §8): let infers when its body does; the
+          -- result substitutes the value and the ⋆-proof away
+          Let a b => do
+            aTy <- kInferE sig ctx a (skelChild 0 sk)
+            let hyp = Prf (Elem.EqTy (CtxVar 0) (substElem a Wk) (substTy aTy Wk))
+            bTy <- kInferE sig (ctx :< aTy :< hyp) b (skelChild 1 sk)
+            pure (substTy bTy (Ext (Ext Id a) Star))
           NatElim z st t =>
             case takeP pMotive sk of
               Just ((mot, motSk), _) => do
diff --git a/src/idris/Nova/Kernel/Beta.idr b/src/idris/Nova/Kernel/Beta.idr
index fd83037..b29bf65 100644
--- a/src/idris/Nova/Kernel/Beta.idr
+++ b/src/idris/Nova/Kernel/Beta.idr
@@ -53,6 +53,10 @@ mutual
     in case betaElem sig f of
          PiIntro g => betaElem sig (substElem g (Ext Id e'))
          f'        => PiApp f' e'
+  -- el-let-beta: a let is ALWAYS a redex — let a b ≜ b[id, a, ⋆]
+  -- (normal forms contain no let)
+  betaElem sig (Let a b) =
+    betaElem sig (substElem b (Ext (Ext Id a) Star))
   betaElem sig (SigmaIntro a b)   = SigmaIntro (betaElem sig a) (betaElem sig b)
   betaElem sig (SigmaElim1 t) =
     case betaElem sig t of
@@ -234,6 +238,9 @@ mutual
     case whnfE sig f of
       PiIntro g => whnfE sig (substElem g (Ext Id e))
       f'        => PiApp f' e
+  whnfE sig (Let a b) =
+    -- el-let-beta: unconditional — no whnf ever returns a let
+    whnfE sig (substElem b (Ext (Ext Id a) Star))
   whnfE sig (SigmaElim1 t) =
     case whnfE sig t of
       SigmaIntro a _ => whnfE sig a
diff --git a/src/idris/Nova/Kernel/Parser.idr b/src/idris/Nova/Kernel/Parser.idr
index 7181881..98564fd 100644
--- a/src/idris/Nova/Kernel/Parser.idr
+++ b/src/idris/Nova/Kernel/Parser.idr
@@ -141,6 +141,10 @@ mutual
             r <- parseElemAtom; space
             t <- parseElemAtom
             pure (SumElim l r t))
+    <|> (do str_ "let"; space
+            a <- parseElemAtom; space
+            b <- parseElemAtom
+            pure (Let a b))
     <|> (do str_ "class"; space; e <- parseElemAtom; pure (Class e))
     <|> (do str_ "ν"; space; f <- parsePolyAtom; pure (Elem.NuTy f))
     <|> (do str_ "out"; space; e <- parseElemAtom; pure (Out e))
diff --git a/src/idris/Nova/Kernel/Subst.idr b/src/idris/Nova/Kernel/Subst.idr
index 83e4bd3..59cfd5f 100644
--- a/src/idris/Nova/Kernel/Subst.idr
+++ b/src/idris/Nova/Kernel/Subst.idr
@@ -58,6 +58,7 @@ mutual
   substElem (NatElim z s t)    sigma = NatElim (substElem z sigma) (substElem s (under (under sigma))) (substElem t sigma)
   substElem (PiIntro f)        sigma = PiIntro (substElem f (under sigma))
   substElem (PiApp f e)        sigma = PiApp (substElem f sigma) (substElem e sigma)
+  substElem (Let a b)          sigma = Let (substElem a sigma) (substElem b (under (under sigma)))
   substElem (SigmaIntro a b)   sigma = SigmaIntro (substElem a sigma) (substElem b sigma)
   substElem (SigmaElim1 t)     sigma = SigmaElim1 (substElem t sigma)
   substElem (SigmaElim2 t)     sigma = SigmaElim2 (substElem t sigma)
@@ -189,6 +190,7 @@ mutual
   strengthenElem d (NatElim z s t)    = NatElim <$> strengthenElem d z <*> strengthenElem (2 + d) s <*> strengthenElem d t
   strengthenElem d (PiIntro f)        = PiIntro <$> strengthenElem (1 + d) f
   strengthenElem d (PiApp f e)        = PiApp <$> strengthenElem d f <*> strengthenElem d e
+  strengthenElem d (Let a b)          = Let <$> strengthenElem d a <*> strengthenElem (2 + d) b
   strengthenElem d (SigmaIntro a b)   = SigmaIntro <$> strengthenElem d a <*> strengthenElem d b
   strengthenElem d (SigmaElim1 t)     = SigmaElim1 <$> strengthenElem d t
   strengthenElem d (SigmaElim2 t)     = SigmaElim2 <$> strengthenElem d t
diff --git a/src/idris/Nova/Kernel/Syntax.idr b/src/idris/Nova/Kernel/Syntax.idr
index 49cd92e..0428501 100644
--- a/src/idris/Nova/Kernel/Syntax.idr
+++ b/src/idris/Nova/Kernel/Syntax.idr
@@ -78,6 +78,12 @@ mutual
       PiIntro : Elem -> Elem
       ||| f e
       PiApp : Elem -> Elem -> Elem
+      ||| let a b  (let-expression: definiens, then body. The body
+      ||| binds the definiens' VALUE and its UNFOLDING EQUATION —
+      ||| Γ ▷ A ▷ Prf (☐₀ ≡ a[↑] ∈ A[↑]), el-let — so the definiendum
+      ||| unfolds judgementally inside it. Always a redex: el-let-beta
+      ||| contracts to b[id, a, ⋆], so normal forms contain no let.)
+      Let : Elem -> Elem -> Elem
       ||| t , t (sigma introduction / pair)
       SigmaIntro : Elem -> Elem -> Elem
       ||| t .π₁  (sigma elimination, first projection)
@@ -424,6 +430,7 @@ mutual
     NatElim z s t    == NatElim z' s' t'   = z == z' && s == s' && t == t'
     PiIntro e        == PiIntro e'         = e == e'
     PiApp f e        == PiApp f' e'         = f == f' && e == e'
+    Let a b          == Let a' b'           = a == a' && b == b'
     SigmaIntro e1 e2 == SigmaIntro e1' e2' = e1 == e1' && e2 == e2'
     SigmaElim1 e     == SigmaElim1 e'      = e == e'
     SigmaElim2 e     == SigmaElim2 e'      = e == e'
@@ -570,6 +577,9 @@ mutual
     compare (PiApp f e)        (PiApp f' e')         = compare f f' <+> compare e e'
     compare (PiApp _ _)        _                    = LT
     compare _                  (PiApp _ _)          = GT
+    compare (Let a b)          (Let a' b')          = compare a a' <+> compare b b'
+    compare (Let _ _)          _                    = LT
+    compare _                  (Let _ _)            = GT
     compare (SigmaIntro e1 e2) (SigmaIntro e1' e2') = compare e1 e1' <+> compare e2 e2'
     compare (SigmaIntro _ _)   _                    = LT
     compare _                  (SigmaIntro _ _)     = GT
@@ -733,6 +743,7 @@ mutual
     show (NatElim z s t) = "NatElim (\{show z}) (\{show s}) (\{show t})"
     show (PiIntro e) = "PiIntro (\{show e})"
     show (PiApp f e) = "PiApp (\{show f}) (\{show e})"
+    show (Let a b) = "Let (\{show a}) (\{show b})"
     show (SigmaIntro e1 e2) = "SigmaIntro (\{show e1}) (\{show e2})"
     show (SigmaElim1 e) = "SigmaElim1 (\{show e})"
     show (SigmaElim2 e) = "SigmaElim2 (\{show e})"
diff --git a/src/nova/letExpr.nova b/src/nova/letExpr.nova
new file mode 100644
index 0000000..768b262
--- /dev/null
+++ b/src/nova/letExpr.nova
@@ -0,0 +1,33 @@
+-- let-expressions: local definitions with judgemental transparency.
+--
+-- The body of `let x ≔ e in b` is typed under x AND its unfolding
+-- equation x ≡ e (docs/NovaFoundation.txt, el-let — the strong,
+-- definition-carrying form), so facts stated at the abbreviation
+-- discharge against facts about its unfolding silently: no manual
+-- unfolding, no transport, no plumbing. From the outside a let IS its
+-- unfolding (el-let-beta), so lemmas about a let-using definition
+-- compute as if the let were never there.
+
+import nat (+)
+
+-- checking mode, nested lets, an annotated definiens
+-- (`let x : T ≔ e in b` is sugar for `let x ≔ (e : T) in b`)
+def four : ℕ ≔
+  let one : ℕ ≔ S Z in
+  let two ≔ one + one in
+  two + two
+
+-- a let in INFERENCE position (an application head): the body's type
+-- is inferred and the definiens substituted back into it
+def three : ℕ ≔ (let f ≔ (λx. S x : ℕ → ℕ) in f) (S (S Z))
+
+-- transparency inside the body: the ⋆ pays an equation stated at the
+-- ABBREVIATION m while the goal is stated at its unfolding — both
+-- gaps close through the let's own hypothesis (m ≡ n + n), not by β
+-- (m is a variable, not a redex)
+def letShared : (n : ℕ) → (n + n) + Z ≡ n + n ∈ ℕ ≔
+  λn. let m ≔ n + n in (⋆ : m + Z ≡ m ∈ ℕ)
+
+-- the outside view: a let-expression is judgementally its unfolding
+def fourUnfolds : four ≡ S (S (S (S Z))) ∈ ℕ ≔ ⋆
+def threeUnfolds : three ≡ S (S (S Z)) ∈ ℕ ≔ ⋆
diff --git a/tests/nova/elaboration/elab-let-accept/expected b/tests/nova/elaboration/elab-let-accept/expected
new file mode 100644
index 0000000..6623eed
--- /dev/null
+++ b/tests/nova/elaboration/elab-let-accept/expected
@@ -0,0 +1,6 @@
+defined plus
+defined letNested
+defined letApp
+defined letShared
+defined letUnfolds
+Accepted.
diff --git a/tests/nova/elaboration/elab-let-accept/input.nova b/tests/nova/elaboration/elab-let-accept/input.nova
new file mode 100644
index 0000000..181de54
--- /dev/null
+++ b/tests/nova/elaboration/elab-let-accept/input.nova
@@ -0,0 +1,18 @@
+def plus : ℕ → ℕ → ℕ ≔ λx. λy. ℕ-elim (n. ℕ) x (n ih. S ih) y
+
+-- checking mode, nested lets, annotated definiens
+def letNested : ℕ ≔
+  let a : ℕ ≔ S Z in
+  let b ≔ plus a a in
+  plus b b
+
+-- let in inference position (application head); body a variable
+def letApp : ℕ ≔ (let f ≔ (λx. S x : ℕ → ℕ) in f) Z
+
+-- transparency: the ⋆ is stated at the ABBREVIATION m, the goal at
+-- its unfolding — both hops walk through the let's own hypothesis
+def letShared : (n : ℕ) → plus (plus n n) Z ≡ plus n n ∈ ℕ ≔
+  λn. let m ≔ plus n n in (⋆ : plus m Z ≡ m ∈ ℕ)
+
+-- the outside view: a let equals its unfolding by β
+def letUnfolds : letNested ≡ plus (plus (S Z) (S Z)) (plus (S Z) (S Z)) ∈ ℕ ≔ ⋆
diff --git a/tests/nova/elaboration/elab-let-accept/run b/tests/nova/elaboration/elab-let-accept/run
new file mode 100755
index 0000000..505e6e2
--- /dev/null
+++ b/tests/nova/elaboration/elab-let-accept/run
@@ -0,0 +1,2 @@
+#!/bin/sh
+"$1" elab input.nova
diff --git a/tests/nova/elaboration/elab-let-obligation/expected b/tests/nova/elaboration/elab-let-obligation/expected
new file mode 100644
index 0000000..3a9c436
--- /dev/null
+++ b/tests/nova/elaboration/elab-let-obligation/expected
@@ -0,0 +1,4 @@
+defined letObl [+1 obligation]
+open obligations (1):
+  [1] (n : ℕ) (m : ℕ) (_ : m ≡ S n ∈ ℕ) ⊢ m ≐ Z : ℕ
+      at: def letObl: checking ⋆
diff --git a/tests/nova/elaboration/elab-let-obligation/input.nova b/tests/nova/elaboration/elab-let-obligation/input.nova
new file mode 100644
index 0000000..2870a78
--- /dev/null
+++ b/tests/nova/elaboration/elab-let-obligation/input.nova
@@ -0,0 +1,5 @@
+-- an unprovable equation paid INSIDE a let body: the obligation's
+-- context shows the let's two entries — the value and its unfolding
+-- hypothesis (rendered as an anonymous Prf entry)
+def letObl : (n : ℕ) → ℕ ≔
+  λn. let m ≔ S n in ((λh. m) : (m ≡ Z ∈ ℕ) → ℕ) ⋆
diff --git a/tests/nova/elaboration/elab-let-obligation/run b/tests/nova/elaboration/elab-let-obligation/run
new file mode 100755
index 0000000..505e6e2
--- /dev/null
+++ b/tests/nova/elaboration/elab-let-obligation/run
@@ -0,0 +1,2 @@
+#!/bin/sh
+"$1" elab input.nova
diff --git a/tests/nova/elaboration/parse-let/expected b/tests/nova/elaboration/parse-let/expected
new file mode 100644
index 0000000..103e28a
--- /dev/null
+++ b/tests/nova/elaboration/parse-let/expected
@@ -0,0 +1 @@
+Let x (Ann (Z) (ℕ)) (S (x@1))
diff --git a/tests/nova/elaboration/parse-let/run b/tests/nova/elaboration/parse-let/run
new file mode 100755
index 0000000..a9e3153
--- /dev/null
+++ b/tests/nova/elaboration/parse-let/run
@@ -0,0 +1,2 @@
+#!/bin/sh
+"$1" run surface-elem "let x : ℕ ≔ Z in S x"
diff --git a/tests/nova/evaluation/eval-let/expected b/tests/nova/evaluation/eval-let/expected
new file mode 100644
index 0000000..fa03e69
--- /dev/null
+++ b/tests/nova/evaluation/eval-let/expected
@@ -0,0 +1 @@
+NatIntro1 (NatIntro1 (NatIntro1 (NatIntro1 (NatIntro0))))
diff --git a/tests/nova/evaluation/eval-let/input.nova b/tests/nova/evaluation/eval-let/input.nova
new file mode 100644
index 0000000..2c3fb4d
--- /dev/null
+++ b/tests/nova/evaluation/eval-let/input.nova
@@ -0,0 +1,4 @@
+def plus : ℕ → ℕ → ℕ ≔ λx. λy. ℕ-elim (n. ℕ) x (n ih. S ih) y
+
+-- a let is always a redex: nf contracts it and shares nothing
+def four : ℕ ≔ let two ≔ S (S Z) in plus two two
diff --git a/tests/nova/evaluation/eval-let/run b/tests/nova/evaluation/eval-let/run
new file mode 100755
index 0000000..8f1d2cc
--- /dev/null
+++ b/tests/nova/evaluation/eval-let/run
@@ -0,0 +1,2 @@
+#!/bin/sh
+"$1" eval input.nova four
diff --git a/tests/nova/parser/elem-let/expected b/tests/nova/parser/elem-let/expected
new file mode 100644
index 0000000..9b9a053
--- /dev/null
+++ b/tests/nova/parser/elem-let/expected
@@ -0,0 +1 @@
+Let (NatIntro0) (NatIntro1 (CtxVar 1))
diff --git a/tests/nova/parser/elem-let/run b/tests/nova/parser/elem-let/run
new file mode 100755
index 0000000..66fb620
--- /dev/null
+++ b/tests/nova/parser/elem-let/run
@@ -0,0 +1,2 @@
+#!/bin/sh
+"$1" run elem "let Z (S ☐₁)"