diff --git a/OctiveLean.lean b/OctiveLean.lean
index dea61dc..f43f509 100644
--- a/OctiveLean.lean
+++ b/OctiveLean.lean
@@ -22,3 +22,4 @@ import OctiveLean.Core.Determinism
 import OctiveLean.Core.Eval
 import OctiveLean.Core.Types
 import OctiveLean.Core.TypeSoundness
+import OctiveLean.Core.Preservation
diff --git a/OctiveLean/Core/Determinism.lean b/OctiveLean/Core/Determinism.lean
index 0ad188e..a003b36 100644
--- a/OctiveLean/Core/Determinism.lean
+++ b/OctiveLean/Core/Determinism.lean
@@ -43,7 +43,8 @@ theorem BigStep.deterministic
     | letInR D1' D2' =>
       have ⟨hv1, hE1⟩ := ih1 D1'
       subst hv1; subst hE1
-      exact ih2 D2'
+      have ⟨hv2, _⟩ := ih2 D2'
+      exact ⟨hv2, rfl⟩
   | ifTR _ _ ihc iht =>
     cases D₂ with
     | ifTR Dc' Dt' =>
diff --git a/OctiveLean/Core/Eval.lean b/OctiveLean/Core/Eval.lean
index 7eab6e0..b2a6360 100644
--- a/OctiveLean/Core/Eval.lean
+++ b/OctiveLean/Core/Eval.lean
@@ -38,7 +38,10 @@ def eval : Nat → Env → Term → Option (Value × Env)
       | _ => none
   | n + 1, env, .letIn x e1 e2 =>
       match eval n env e1 with
-      | some (v1, env1) => eval n (env1.extend x v1) e2
+      | some (v1, env1) =>
+          match eval n (env1.extend x v1) e2 with
+          | some (v2, _) => some (v2, env1)   -- scope-restore: discard body's post-env
+          | none         => none
       | none            => none
   | n + 1, env, .ifte ec e1 e2 =>
       match eval n env ec with
@@ -113,7 +116,11 @@ theorem eval_sound :
       simp only [eval] at heq
       split at heq
       next v1 env1 heq1 =>
-        exact .letInR (ih _ _ _ _ heq1) (ih _ _ _ _ heq)
+        split at heq
+        next v2 _ heq2 =>
+          simp at heq; obtain ⟨rfl, rfl⟩ := heq
+          exact .letInR (ih _ _ _ _ heq1) (ih _ _ _ _ heq2)
+        next => simp at heq
       next => simp at heq
     | ifte ec e1 e2 =>
       simp only [eval] at heq
diff --git a/OctiveLean/Core/Preservation.lean b/OctiveLean/Core/Preservation.lean
new file mode 100644
index 0000000..6cfa50b
--- /dev/null
+++ b/OctiveLean/Core/Preservation.lean
@@ -0,0 +1,118 @@
+import OctiveLean.Core.TypeSoundness
+
+namespace OctiveLean.Core
+
+/-! # Preservation theorem for TOC big-step semantics.
+
+  `Γ ⊢ e : T  ∧  HasTypeEnv env Γ  ∧  BigStep env e v env'
+     ⟹  HasTypeV v T  ∧  HasTypeEnv env' Γ`
+
+Compare with TGC's preservation: there's no heap-typing extension, no
+heap-update lemmas — the state is just the env. Γ is unchanged by big
+steps (`assign` requires `x` already typed; mutates value only).
+
+`letIn` has scope-restoring semantics — its post-env is the env after
+evaluating the bound expression, not after evaluating the body. This
+differs from TGC's letIn (which has no env to leak) and is what makes
+preservation provable in the presence of mutation. -/
+
+/-! ## Inversion for binop typing — same shape as TGC's. -/
+
+theorem binop_apply_sound
+    {op : BinOp} {v1 v2 v : Value} {T1 T2 T : Ty}
+    (hOp : op.typeOf T1 T2 = some T)
+    (hV1 : HasTypeV v1 T1) (hV2 : HasTypeV v2 T2)
+    (hApp : op.apply v1 v2 = some v) :
+    HasTypeV v T := by
+  cases op <;> cases T1 <;> cases T2 <;> simp [BinOp.typeOf] at hOp <;>
+    (try (cases hOp; cases hV1; cases hV2; simp [BinOp.apply] at hApp; cases hApp; constructor))
+
+/-! ## Preservation. -/
+
+theorem preservation :
+    ∀ {env e v env'} (_D : BigStep env e v env')
+      {Γ T} (_hT : HasType Γ e T) (_hE : HasTypeEnv env Γ),
+      HasTypeV v T ∧ HasTypeEnv env' Γ := by
+  intros env e v env' D
+  induction D with
+  | unitR =>
+    intros Γ T hT hE; cases hT; exact ⟨.vUnit, hE⟩
+  | intLitR n =>
+    intros Γ T hT hE; cases hT; exact ⟨.vInt n, hE⟩
+  | boolLitR b =>
+    intros Γ T hT hE; cases hT; exact ⟨.vBool b, hE⟩
+  | varR hLook =>
+    intros Γ T hT hE
+    cases hT with
+    | var hLookT =>
+      have ⟨v', hLook', hTV⟩ := hE _ _ hLookT
+      rw [hLook] at hLook'; cases hLook'
+      exact ⟨hTV, hE⟩
+  | lamR x body =>
+    intros Γ T hT hE
+    cases hT with
+    | lam hBody => exact ⟨HasTypeV.vClos_of_env hE hBody, hE⟩
+  | appR _ _ _ ih1 ih2 ihb =>
+    intros Γ T hT hE
+    cases hT with
+    | app hT1 hT2 =>
+      have ⟨hClosT, hE1⟩ := ih1 hT1 hE
+      have ⟨hArgT, hE2⟩ := ih2 hT2 hE1
+      have ⟨_, _, _, hArrow, hE_clos, hBody⟩ := hClosT.vClos_to_env
+      cases hArrow
+      have ⟨hValT, _⟩ := ihb hBody (hE_clos.extend_letIn hArgT)
+      exact ⟨hValT, hE2⟩
+  | letInR _ _ ih1 ih2 =>
+    intros Γ T hT hE
+    cases hT with
+    | letIn hT1 hT2 =>
+      have ⟨hV1, hE1⟩ := ih1 hT1 hE
+      have ⟨hV2, _⟩ := ih2 hT2 (hE1.extend_letIn hV1)
+      exact ⟨hV2, hE1⟩
+  | ifTR _ _ ihc iht =>
+    intros Γ T hT hE
+    cases hT with
+    | ifte hTc hT1 _ =>
+      have ⟨_, hE1⟩ := ihc hTc hE
+      exact iht hT1 hE1
+  | ifFR _ _ ihc ihf =>
+    intros Γ T hT hE
+    cases hT with
+    | ifte hTc _ hT2 =>
+      have ⟨_, hE1⟩ := ihc hTc hE
+      exact ihf hT2 hE1
+  | binopR _ _ Hop ih1 ih2 =>
+    intros Γ T hT hE
+    cases hT with
+    | binop hT1 hT2 hOpT =>
+      have ⟨hV1, hE1⟩ := ih1 hT1 hE
+      have ⟨hV2, hE2⟩ := ih2 hT2 hE1
+      exact ⟨binop_apply_sound hOpT hV1 hV2 Hop, hE2⟩
+  | seqR _ _ ih1 ih2 =>
+    intros Γ T hT hE
+    cases hT with
+    | seq hT1 hT2 =>
+      have ⟨_, hE1⟩ := ih1 hT1 hE
+      exact ih2 hT2 hE1
+  | assignR _ ih =>
+    intros Γ T hT hE
+    cases hT with
+    | assign hx hT1 =>
+      have ⟨hV, hE1⟩ := ih hT1 hE
+      exact ⟨.vUnit, hE1.extend_typed hx hV⟩
+  | whileFR _ ihc =>
+    intros Γ T hT hE
+    cases hT with
+    | whileT hTc _ =>
+      have ⟨_, hE1⟩ := ihc hTc hE
+      exact ⟨.vUnit, hE1⟩
+  | whileTR _ _ _ ihc ihb ihw =>
+    intros Γ T hT hE
+    cases hT with
+    | whileT hTc hTb =>
+      have ⟨_, hE1⟩ := ihc hTc hE
+      have ⟨_, hE2⟩ := ihb hTb hE1
+      -- Reconstruct typing for the recursive while step.
+      exact ihw (HasType.whileT hTc hTb) hE2
+
+end OctiveLean.Core
diff --git a/OctiveLean/Core/Semantics.lean b/OctiveLean/Core/Semantics.lean
index b0dc31b..85a760e 100644
--- a/OctiveLean/Core/Semantics.lean
+++ b/OctiveLean/Core/Semantics.lean
@@ -73,7 +73,7 @@ inductive BigStep : Env → Term → Value → Env → Prop where
   | letInR   {env x e1 e2 v1 v2 env1 env2}
              (D1 : BigStep env  e1 v1 env1)
              (D2 : BigStep (env1.extend x v1) e2 v2 env2) :
-      BigStep env (.letIn x e1 e2) v2 env2
+      BigStep env (.letIn x e1 e2) v2 env1
   | ifTR     {env ec e1 e2 v env1 env2}
              (Dc : BigStep env  ec (.vBool true) env1)
              (Dt : BigStep env1 e1 v env2) :
diff --git a/OctiveLean/Core/TypeSoundness.lean b/OctiveLean/Core/TypeSoundness.lean
index 3cc9c15..2d2abb2 100644
--- a/OctiveLean/Core/TypeSoundness.lean
+++ b/OctiveLean/Core/TypeSoundness.lean
@@ -92,4 +92,22 @@ theorem HasTypeV.vClos_of_env
     exact hVT'
   · exact hb
 
+/-- Inversion of `HasTypeV` for closure values. Exposes the closure's
+    typing context and the function-form `HasTypeEnv`. -/
+theorem HasTypeV.vClos_to_env
+    {x : String} {body : Term} {env : Env} {T : Ty}
+    (h : HasTypeV (.vClos x body env) T) :
+    ∃ Γ T_arg T_ret, T = .arrow T_arg T_ret ∧
+      HasTypeEnv env Γ ∧
+      HasType (Γ.extend x T_arg) body T_ret := by
+  cases h with
+  | vClos he_dom he_typed hBody =>
+    refine ⟨_, _, _, rfl, ?_, hBody⟩
+    intro y T_y hLy
+    have hdom := he_dom y T_y hLy
+    cases hLE : env.lookup y with
+    | none => rw [hLE] at hdom; cases hdom
+    | some v_y =>
+      exact ⟨v_y, rfl, he_typed y T_y v_y hLy hLE⟩
+
 end OctiveLean.Core