diff --git a/Cslib.lean b/Cslib.lean
index b504973c3..34e4f1e60 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -89,6 +89,7 @@ public import Cslib.Foundations.Semantics.LTS.Union
 public import Cslib.Foundations.Syntax.Congruence
 public import Cslib.Foundations.Syntax.Context
 public import Cslib.Foundations.Syntax.HasAlphaEquiv
+public import Cslib.Foundations.Syntax.HasParallelSubstitution
 public import Cslib.Foundations.Syntax.HasSubstitution
 public import Cslib.Foundations.Syntax.HasWellFormed
 public import Cslib.Init
@@ -122,9 +123,10 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
-public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.ParallelSubst
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.SubstEnv
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
 public import Cslib.Logics.HML.Basic
 public import Cslib.Logics.HML.LogicalEquivalence
diff --git a/Cslib/Foundations/Syntax/HasParallelSubstitution.lean b/Cslib/Foundations/Syntax/HasParallelSubstitution.lean
new file mode 100644
index 000000000..394e5a488
--- /dev/null
+++ b/Cslib/Foundations/Syntax/HasParallelSubstitution.lean
@@ -0,0 +1,156 @@
+/-
+Copyright (c) 2026 David Wegmann. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Claude Opus 4.7 (via Claude Code), David Wegmann
+-/
+
+module
+
+public import Cslib.Init
+
+/-! # Parallel (simultaneous) substitution
+
+A typeclass for *parallel* substitution: replacing every variable of a term
+simultaneously, according to an assignment `σ : Var → T`, in a single pass.
+
+This is the operation needed by first-order unification — where a unifier is a
+simultaneous assignment and most-general-unifier reasoning relies on substitution
+composition — and it subsumes the finite multi-substitution used elsewhere (e.g.
+the strong-normalization proof), which is recovered by turning a finite
+`Context` into a total assignment.
+
+Unlike `Cslib.HasSubstitution` (single-variable replacement `t[x := t']`),
+parallel substitution is *not* derivable from iterated single substitutions:
+applying bindings one at a time is sequential, whereas here all variables are
+replaced at once.
+
+## Operation vs. laws
+
+Following the `Monad` / `LawfulMonad` pattern (and mirroring `Cslib.HasSubstitution`,
+which is a pure notation typeclass), the operation and its laws are split:
+
+* `HasParallelSubstitution` carries only `var` and `psubst`, plus notation.
+* `LawfulHasParallelSubstitution` carries the laws.
+
+A syntax with variables that satisfies the laws is exactly a (relative) monad:
+`var` is the unit (`return`) and `psubst` is the Kleisli extension (`bind`, with
+arguments flipped). In particular `psubst_comp` is associativity, which gives
+substitution *composition* `t⟦τ⟧ₚ⟦σ⟧ₚ = t⟦σ ∘ₚ τ⟧ₚ` — the algebra the MGU proof
+rests on. The laws hold unconditionally for capture-free representations
+(first-order terms, locally-nameless λ-terms); named representations, whose
+substitution is only well-behaved up to α-equivalence, are deliberately not
+expected to be lawful instances.
+-/
+
+public section
+
+namespace Cslib
+
+universe u v
+
+/-- Types `T` whose values are syntax over variables of type `Var`, equipped with
+*parallel* (simultaneous) substitution.
+
+`var` embeds a variable as a value; `psubst σ t` replaces every variable `x`
+occurring in `t` by `σ x`, all at once. This is a pure notation/operation class;
+the substitution laws live in `LawfulHasParallelSubstitution`. -/
+class HasParallelSubstitution (T : Type u) (Var : outParam (Type v)) where
+  /-- Embed a variable as a value. -/
+  var : Var → T
+  /-- Simultaneously replace every variable `x` in `t` by `σ x`. -/
+  psubst : (Var → T) → T → T
+
+namespace HasParallelSubstitution
+
+/-- Notation for parallel substitution, `t⟦σ⟧ₚ`: apply assignment `σ` to `t`. -/
+scoped notation:max t "⟦" σ "⟧ₚ" => HasParallelSubstitution.psubst σ t
+
+variable {T : Type u} {Var : Type v} [HasParallelSubstitution T Var]
+
+/-- Kleisli composition of assignments: `(σ ∘ₚ τ) x = (τ x)⟦σ⟧ₚ`, i.e. apply `τ`
+first, then `σ`. -/
+def comp (σ τ : Var → T) : Var → T := fun x => psubst σ (τ x)
+
+@[inherit_doc]
+scoped infixr:90 " ∘ₚ " => comp
+
+/-- `σ` is at least as general as `τ` (written `σ ≤ₚ τ`) when `τ` factors through
+`σ`: there is an assignment `ρ` with `τ = ρ ∘ₚ σ`, i.e. `τ x = (σ x)⟦ρ⟧ₚ` for
+every variable `x`. Equivalently, in the "apply to every term" formulation (see
+`moreGeneral_iff`), applying `τ` to any term equals applying `σ` and then `ρ`.
+
+This is the standard "more general than" relation underlying most-general
+unifiers. In the usual textbook notation, where the composite `στ` applies `σ`
+first and then `τ`, it reads `σ ≤ₚ τ ↔ ∃ ρ, τ = σρ`; we write the same thing
+with the (right-to-left) Kleisli composite `ρ ∘ₚ σ`. The relation is taken over
+total assignments — there is deliberately no restriction to a finite domain.
+
+This needs only the operation to *state*; that it is a preorder needs the laws. -/
+def MoreGeneral (σ τ : Var → T) : Prop := ∃ ρ : Var → T, τ = ρ ∘ₚ σ
+
+@[inherit_doc]
+scoped infix:50 " ≤ₚ " => MoreGeneral
+
+end HasParallelSubstitution
+
+open HasParallelSubstitution in
+/-- The laws of parallel substitution: a lawful instance is exactly a (relative)
+monad with `var` as unit and `psubst` as Kleisli extension. Stated as a `Prop`
+class over an existing `HasParallelSubstitution`, mirroring `LawfulMonad`. -/
+class LawfulHasParallelSubstitution (T : Type u) (Var : outParam (Type v))
+    [HasParallelSubstitution T Var] : Prop where
+  /-- Substituting into a single variable looks it up in the assignment.
+  (Monad left identity: `bind (pure x) σ = σ x`.) -/
+  psubst_var : ∀ (σ : Var → T) (x : Var), psubst σ (var x) = σ x
+  /-- The identity assignment `var` acts as the identity substitution.
+  (Monad right identity: `bind t pure = t`.) -/
+  psubst_id : ∀ (t : T), psubst var t = t
+  /-- Substitutions compose into a single pass.
+  (Monad associativity.) -/
+  psubst_comp : ∀ (σ τ : Var → T) (t : T),
+    psubst σ (psubst τ t) = psubst (fun x => psubst σ (τ x)) t
+
+namespace HasParallelSubstitution
+
+variable {T : Type u} {Var : Type v}
+  [HasParallelSubstitution T Var] [LawfulHasParallelSubstitution T Var]
+
+export LawfulHasParallelSubstitution (psubst_var psubst_id psubst_comp)
+
+/-- Substitution composition, stated via `comp`: substituting by `τ` and then `σ`
+is one substitution by `σ ∘ₚ τ`. -/
+theorem psubst_psubst (σ τ : Var → T) (t : T) :
+    psubst σ (psubst τ t) = psubst (σ ∘ₚ τ) t :=
+  psubst_comp σ τ t
+
+/-- Term-level characterization of generality, matching the "apply to every term"
+formulation used for unifiers: `σ ≤ₚ τ` iff there is `ρ` with
+`t⟦τ⟧ₚ = (t⟦σ⟧ₚ)⟦ρ⟧ₚ` for all terms `t`. The forward direction is `psubst_comp`;
+the backward direction instantiates at `t = var x` and uses `psubst_var`. -/
+theorem moreGeneral_iff {σ τ : Var → T} :
+    σ ≤ₚ τ ↔ ∃ ρ : Var → T, ∀ t : T, psubst τ t = psubst ρ (psubst σ t) := by
+  constructor
+  · rintro ⟨ρ, rfl⟩
+    exact ⟨ρ, fun t => (psubst_comp ρ σ t).symm⟩
+  · rintro ⟨ρ, h⟩
+    refine ⟨ρ, ?_⟩
+    funext x
+    simpa [comp, psubst_var] using h (var x)
+
+/-- Generality is reflexive: the identity assignment `var` witnesses `σ ≤ₚ σ`. -/
+@[refl]
+theorem MoreGeneral.refl (σ : Var → T) : σ ≤ₚ σ :=
+  ⟨var, by funext x; simp [comp, psubst_id]⟩
+
+/-- Generality is transitive: compose the two witnessing assignments. -/
+theorem MoreGeneral.trans {σ τ υ : Var → T} (h₁ : σ ≤ₚ τ) (h₂ : τ ≤ₚ υ) : σ ≤ₚ υ := by
+  obtain ⟨ρ₁, rfl⟩ := h₁
+  obtain ⟨ρ₂, rfl⟩ := h₂
+  refine ⟨ρ₂ ∘ₚ ρ₁, ?_⟩
+  funext x
+  simp only [comp]
+  exact psubst_comp ρ₂ ρ₁ (σ x)
+
+end HasParallelSubstitution
+
+end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
index 9c98b17da..525b20a5b 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
@@ -12,7 +12,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
-public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.SubstEnv
 
 /-! Strong normalization (termination) for full beta-reduction of simply typed lambda calculus. -/
 
@@ -74,10 +74,12 @@ lemma semanticMap_saturated (τ : Ty Base) : @Saturated Var (semanticMap τ) :=
 /-- The `entails_context` predicate ensures that each variable in the context
     is mapped to a term in the corresponding semantic map. -/
 abbrev entails_context (E : Term.Env Var) (Γ : Context Var (Ty Base)) :=
-  ∀ {x τ}, ⟨x, τ⟩ ∈ Γ → (multiSubst E (fvar x)) ∈ semanticMap τ
+  ∀ {x τ}, ⟨x, τ⟩ ∈ Γ → (E.toAssignment x) ∈ semanticMap τ
 
 /-- The empty context is entailed by any environment. -/
-lemma entails_context_empty {Γ : Context Var (Ty Base)} : entails_context [] Γ := by
+lemma entails_context_empty {Γ : Context Var (Ty Base)} : entails_context Env.empty Γ := by
+  intro x τ _
+  rw [Env.empty_toAssignment]
   have := semanticMap_saturated (Var := Var) (Base := Base)
   grind
 
@@ -90,36 +92,45 @@ lemma entails_context_cons (E : Term.Env Var) (Γ : Context Var (Ty Base))
     (x : Var) (τ : Ty Base) (sub : Term Var)
     (h_fresh : x ∉ E.dom ∪ E.fv ∪ Γ.dom)
     (h_mem : sub ∈ semanticMap τ) :
-    entails_context E Γ → entails_context (⟨ x, sub ⟩ :: E) (⟨ x, τ ⟩ :: Γ) := by
-  grind [multiSubst_fvar_fresh, subst_fresh, multiSubst_preserves_not_fvar]
+    entails_context E Γ → entails_context (E.update x sub) (⟨ x, τ ⟩ :: Γ) := by
+  intro hE x' τ' hmem
+  rcases List.mem_cons.mp hmem with h | h
+  · simp only [Sigma.mk.injEq, heq_eq_eq] at h
+    obtain ⟨rfl, rfl⟩ := h
+    rw [Env.update_toAssignment, Function.update_self]
+    exact h_mem
+  · have hx' : x' ≠ x := by grind
+    rw [Env.update_toAssignment, Function.update_of_ne hx']
+    exact hE h
 
 /-- The `entails` predicate states that a term `t` is
     semantically valid with respect to a context `Γ` and a type `τ` -/
 abbrev entails (Γ : Context Var (Ty Base)) (t : Term Var) (τ : Ty Base) :=
-    ∀ E, env_LC E → (entails_context E Γ) → (multiSubst E t) ∈ semanticMap τ
+    ∀ E, env_LC E → (entails_context E Γ) → (psubst E.toAssignment t) ∈ semanticMap τ
 
 /-- The `soundness` lemma states that if a term `t` has type `τ` in context `Γ`,
     then `t` is semantically valid with respect to `Γ` and `τ` -/
 lemma soundness {Γ : Context Var (Ty Base)} (derivation_t : Γ ⊢ t ∶ τ) : entails Γ t τ := by
   induction derivation_t with
-  | var Γ xσ_mem_Γ => grind
+  | var Γ xσ_mem_Γ => grind [psubst_fvar]
   | @abs σ Γ t τ L HL IH =>
     intro E _ _ s
     have sat_semMap_σ := semanticMap_saturated (Var := Var) σ
     have sat_semMap_τ := semanticMap_saturated (Var := Var) τ
-    have := sat_semMap_τ.multiApp (multiSubst E t) s []
-    let := multiSubst E t
+    have := sat_semMap_τ.multiApp (psubst E.toAssignment t) s []
+    let := psubst E.toAssignment t
     have ⟨x, _⟩ := fresh_exists <| E.dom ∪ free_union [fv, Context.dom, Env.fv] Var
-    have := IH (x := x) (E := ⟨x,s⟩ :: E)
-    grind [multiSubst_abs, entails_context_cons, multiSubst_open_var]
-  | app => grind [multiSubst_app]
+    have := IH (x := x) (E := E.update x s)
+    grind [psubst_update, entails_context_cons, psubst_open_var, psubst_abs, env_LC_update]
+  | app => grind [psubst_app]
 
 /-- Using soundness and the fact that the empty context
     is entailed by any environment, we can conclude that
     a well-typed term is strongly normalizing. -/
 theorem strong_norm {t : Term Var} {τ : Ty Base} (der : Γ ⊢ t ∶ τ) : SN FullBeta t := by
   apply (semanticMap_saturated τ).sn
-  apply (soundness der [] (by grind) entails_context_empty)
+  have h := soundness der Env.empty env_LC_empty entails_context_empty
+  rwa [Env.empty_toAssignment, psubst_fvar_id] at h
 
 end LambdaCalculus.LocallyNameless.Stlc
 
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean
deleted file mode 100644
index 05db5bab3..000000000
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean
+++ /dev/null
@@ -1,90 +0,0 @@
-/-
-Copyright (c) 2025 David Wegmann. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: David Wegmann
--/
-
-
-module
-
-public import Cslib.Foundations.Data.Relation
-public import Cslib.Foundations.Data.HasFresh
-public import Cslib.Foundations.Syntax.HasSubstitution
-public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
-public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
-
-/-! Multiple substitution for untyped lambda calculus. -/
-
-@[expose] public section
-
-namespace Cslib
-
-universe u v
-
-
-namespace LambdaCalculus.LocallyNameless.Untyped.Term
-
-open scoped Context
-
-variable {Var : Type u} {Base : Type v} [DecidableEq Var]
-
-/-- An environment in context of multi substitution is a list of pairs of
-    variable targets and terms to be substituted for that target -/
-abbrev Env (Var : Type u) := Context Var (Term Var)
-
-/-- Multi-substitution substitutes all target variables
-    in an environment by their corresponding terms -/
-@[scoped grind =]
-def multiSubst (E : Env Var) (M : Term Var) : Term Var :=
-  match E with
-  | [] => M
-  | ⟨i, sub⟩ :: E' => (multiSubst E' M) [ i := sub ]
-
-/-- The free variables of an environment are the union of
-    the free variables of all terms in the environment.
-    The target variables are not necessarily included -/
-def Env.fv (E : Env Var) : Finset Var :=
-  match E with
-  | [] => {}
-  | ⟨ _, sub ⟩ :: E' => sub.fv ∪ Env.fv E'
-
-attribute [scoped grind =] Env.fv
-
-/-- An environment is locally closed if all terms in the environment are locally closed -/
-abbrev env_LC (E : Env Var) : Prop := ∀ {x M}, ⟨x, M⟩ ∈ E → LC M
-
-/-- Adding a locally closed term to an environment preserves local closure -/
-lemma env_LC_cons (lc_sub : LC sub) (lc_E : env_LC E) : env_LC (⟨ x, sub ⟩ :: E) := by
-  grind
-
-/-- Multi-substitution of a fresh variable does nothing -/
-lemma multiSubst_fvar_fresh (E : Env Var) : ∀ x ∉ E.dom, multiSubst E (fvar x) = fvar x := by
-  induction E with grind
-
-/-- If x is neither a free variable of an environment Ns or a term M, then
-    x is also not a free variable of the multi-substitution of Ns into M -/
-lemma multiSubst_preserves_not_fvar (M : Term Var) (E : Env Var) (nmem : x ∉ M.fv ∪ E.fv) :
-    x ∉ (multiSubst E M).fv := by
-  induction E with grind [subst_preserve_not_fvar]
-
-/-- Multi-substitution propagates recursively through an application -/
-lemma multiSubst_app (M N : Term Var) (E : Env Var) :
-    multiSubst E (app M N) = app (multiSubst E M) (multiSubst E N) := by
-  induction E with grind
-
-/-- Multi-substitution propagates recursively through an abstraction -/
-lemma multiSubst_abs (M : Term Var) (E : Env Var) :
-    multiSubst E (abs M) = abs (multiSubst E M) := by
-  induction E with grind
-
-/-- Multi-substitution commutes with opening a term with a fresh variable,
-    provided that the variable is not in the domain of the environment
-    and the environment is locally closed -/
-lemma multiSubst_open_var [HasFresh Var] (M : Term Var) (E : Env Var) (x : Var)
-  (h_ndom : x ∉ E.dom) (h_lc : env_LC E) :
-    multiSubst E (M ^ fvar x) = multiSubst E M ^ fvar x := by
-  induction E with grind
-
-end LambdaCalculus.LocallyNameless.Untyped.Term
-
-end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/ParallelSubst.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/ParallelSubst.lean
new file mode 100644
index 000000000..4b49857b6
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/ParallelSubst.lean
@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2026 David Wegmann. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Claude Opus 4.7 (via Claude Code), David Wegmann
+-/
+
+module
+
+public import Cslib.Foundations.Syntax.HasParallelSubstitution
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
+
+/-! # Parallel substitution for locally-nameless untyped λ-terms
+
+PROTOTYPE: instantiates `HasParallelSubstitution` / `LawfulHasParallelSubstitution`
+for the locally-nameless untyped `Term`, to test how the interface maps onto the
+existing definitions. Not yet wired into the import tree.
+
+Because the representation is locally nameless — bound variables are de Bruijn
+indices and only free variables (`fvar`) are substituted — parallel substitution
+is purely structural and capture-free, so the instance needs **no** typeclass
+constraints (no `DecidableEq`, no `HasFresh`), exactly like the single-variable
+`HasSubstitution` instance for this `Term`.
+
+We also show that the existing single-variable `Term.subst` is the special case
+of `psubst` at a point-updated assignment (`subst_eq_psubst`).
+-/
+
+@[expose] public section
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u}
+
+namespace LambdaCalculus.LocallyNameless.Untyped.Term
+
+/-- Parallel (simultaneous) substitution of free variables: replace every `fvar x`
+by `σ x`, in a single structural pass. Capture-free by local namelessness. -/
+@[scoped grind =]
+def psubst (σ : Var → Term Var) : Term Var → Term Var
+  | bvar i  => bvar i
+  | fvar x  => σ x
+  | app l r => app (psubst σ l) (psubst σ r)
+  | abs M   => abs (psubst σ M)
+
+@[simp] theorem psubst_bvar (σ : Var → Term Var) (i : ℕ) : psubst σ (bvar i) = bvar i := rfl
+@[simp] theorem psubst_fvar (σ : Var → Term Var) (x : Var) : psubst σ (fvar x) = σ x := rfl
+@[simp] theorem psubst_app (σ : Var → Term Var) (l r : Term Var) :
+    psubst σ (app l r) = app (psubst σ l) (psubst σ r) := rfl
+@[simp] theorem psubst_abs (σ : Var → Term Var) (M : Term Var) :
+    psubst σ (abs M) = abs (psubst σ M) := rfl
+
+/-- Substituting every free variable by itself is the identity. -/
+@[simp] theorem psubst_fvar_id (M : Term Var) : psubst fvar M = M := by
+  induction M <;> simp_all
+
+/-- The operation instance: `var` is `fvar`, `psubst` is the structural pass above.
+Note the complete absence of constraints on `Var`. -/
+instance instHasParallelSubstitution : HasParallelSubstitution (Term Var) Var where
+  var := fvar
+  psubst := Term.psubst
+
+/-- The typeclass operation reduces to the concrete `Term.psubst` (definitionally).
+Lets `simp`/`grind` see through the typeclass projection. -/
+@[simp] theorem psubst_eq (σ : Var → Term Var) (M : Term Var) :
+    HasParallelSubstitution.psubst σ M = Term.psubst σ M := rfl
+
+/-- The laws hold unconditionally: this `Term` (with `fvar`/`psubst`) is a lawful
+parallel-substitution structure — i.e. a relative monad on free variables. -/
+instance instLawfulHasParallelSubstitution : LawfulHasParallelSubstitution (Term Var) Var where
+  psubst_var _ _ := rfl
+  psubst_id := fun t => by
+    change Term.psubst fvar t = t
+    induction t <;> simp_all
+  psubst_comp := fun σ τ t => by
+    change Term.psubst σ (Term.psubst τ t) = Term.psubst (fun x => Term.psubst σ (τ x)) t
+    induction t <;> simp_all
+
+/-- The existing single-variable substitution `m[x := sub]` is the special case of
+`psubst` where the assignment is `fvar` updated at `x` to `sub`. This is how the
+two interfaces line up. -/
+theorem subst_eq_psubst [DecidableEq Var] (m : Term Var) (x : Var) (sub : Term Var) :
+    m.subst x sub = psubst (fun y => if x = y then sub else fvar y) m := by
+  induction m <;> simp_all [Term.subst]
+
+end LambdaCalculus.LocallyNameless.Untyped.Term
+
+end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/SubstEnv.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/SubstEnv.lean
new file mode 100644
index 000000000..b23ebcac1
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/SubstEnv.lean
@@ -0,0 +1,138 @@
+/-
+Copyright (c) 2025 David Wegmann. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Claude Opus 4.7 (via Claude Code), David Wegmann
+-/
+
+
+module
+
+public import Cslib.Foundations.Data.HasFresh
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.ParallelSubst
+
+/-! # Substitution environments for untyped lambda calculus
+
+A substitution *environment* is a **finitely-supported assignment** `Var → Term Var`:
+the assignment itself, together with a `Finset` of variables outside which it acts as
+the identity. "Applying an environment" is just the parallel substitution
+`Term.psubst E.toAssignment` — there is no separate multi-substitution operation.
+
+The finite support is what lets the strong-normalization proof pick variables fresh
+for the substitution. Because the support is carried in the structure, the
+domain/free-variable lemmas are immediate (no induction).
+-/
+
+@[expose] public section
+
+namespace Cslib
+
+universe u
+
+namespace LambdaCalculus.LocallyNameless.Untyped.Term
+
+variable {Var : Type u}
+
+/-- A substitution environment: a finitely-supported assignment of terms to variables.
+`support` over-approximates the set of variables the assignment moves. -/
+structure Env (Var : Type u) where
+  /-- The underlying assignment. -/
+  toAssignment : Var → Term Var
+  /-- A finite superset of the variables actually moved by the assignment. -/
+  support : Finset Var
+  /-- Outside the support, the assignment is the identity. -/
+  mem_support : ∀ {x : Var}, toAssignment x ≠ fvar x → x ∈ support
+
+namespace Env
+
+/-- The domain of an environment: the variables it (potentially) moves. -/
+def dom (E : Env Var) : Finset Var := E.support
+
+/-- The free variables occurring in the terms the environment substitutes. -/
+def fv [DecidableEq Var] (E : Env Var) : Finset Var :=
+  E.support.biUnion (fun x => (E.toAssignment x).fv)
+
+/-- The identity environment, leaving every variable untouched. -/
+def empty : Env Var := ⟨fvar, ∅, fun h => absurd rfl h⟩
+
+@[simp] lemma empty_toAssignment : (empty : Env Var).toAssignment = fvar := rfl
+
+/-- Extend an environment with a new binding `x ↦ s`. -/
+def update [DecidableEq Var] (E : Env Var) (x : Var) (s : Term Var) : Env Var where
+  toAssignment := Function.update E.toAssignment x s
+  support := insert x E.support
+  mem_support := by
+    intro y hy
+    by_cases h : y = x
+    · subst h; exact Finset.mem_insert_self _ _
+    · rw [Function.update_of_ne h] at hy
+      exact Finset.mem_insert_of_mem (E.mem_support hy)
+
+@[simp] lemma update_toAssignment [DecidableEq Var] (E : Env Var) (x : Var) (s : Term Var) :
+    (E.update x s).toAssignment = Function.update E.toAssignment x s := rfl
+
+end Env
+
+/-- An environment is locally closed if every variable maps to a locally closed term. -/
+def env_LC (E : Env Var) : Prop := ∀ x, (E.toAssignment x).LC
+
+lemma env_LC_empty : env_LC (Env.empty : Env Var) := fun x => by simpa using LC.fvar x
+
+lemma env_LC_update [DecidableEq Var] {E : Env Var} {x : Var} {s : Term Var}
+    (lc_s : LC s) (lc_E : env_LC E) : env_LC (E.update x s) := by
+  intro y
+  rw [Env.update_toAssignment]
+  by_cases h : y = x
+  · subst h; rwa [Function.update_self]
+  · rw [Function.update_of_ne h]; exact lc_E y
+
+/-! ## Assignment lemmas -/
+
+/-- Outside its domain, the assignment is the identity. Immediate from `mem_support`. -/
+lemma toAssignment_fresh {E : Env Var} {x : Var} (h : x ∉ E.dom) : E.toAssignment x = fvar x := by
+  by_contra hc
+  exact h (E.mem_support hc)
+
+/-- A locally closed environment maps every variable to a locally closed term. -/
+lemma toAssignment_lc {E : Env Var} (h : env_LC E) (x : Var) : LC (E.toAssignment x) := h x
+
+/-- If `x` is fresh for the environment and distinct from `y`, then it does not occur
+free in the term `y` maps to. -/
+lemma toAssignment_not_fvar [DecidableEq Var] {E : Env Var} {x y : Var}
+    (hx : x ∉ E.fv) (hxy : x ≠ y) : x ∉ (E.toAssignment y).fv := by
+  by_cases hy : y ∈ E.support
+  · exact fun hc => hx (Finset.mem_biUnion.mpr ⟨y, hy, hc⟩)
+  · rw [toAssignment_fresh hy]; simpa using hxy
+
+/-! ## Substitution lemmas -/
+
+/-- Parallel substitution by an assignment of locally closed terms commutes with
+opening. -/
+lemma psubst_openRec [HasFresh Var] (σ : Var → Term Var) (lc : ∀ y, LC (σ y)) :
+    ∀ (k : ℕ) (u e : Term Var), psubst σ (e⟦k ↝ u⟧) = (psubst σ e)⟦k ↝ psubst σ u⟧ := by
+  intro k u e
+  induction e generalizing k with
+    grind [openRec_bvar, openRec_fvar, openRec_app, openRec_abs,
+      psubst_bvar, psubst_fvar, psubst_app, psubst_abs]
+
+/-- Applying an environment commutes with opening by a fresh variable, provided the
+environment is locally closed. -/
+lemma psubst_open_var [HasFresh Var] (M : Term Var) (E : Env Var) (x : Var)
+    (h_ndom : x ∉ E.dom) (h_lc : env_LC E) :
+    psubst E.toAssignment (M ^ fvar x) = psubst E.toAssignment M ^ fvar x := by
+  simp only [open']
+  rw [psubst_openRec E.toAssignment h_lc, psubst_fvar, toAssignment_fresh h_ndom]
+
+/-- Extending with a binding `x ↦ s` fresh for the environment is the same as applying
+the environment and then substituting `x` by `s`. -/
+lemma psubst_update [DecidableEq Var] {x : Var} (s : Term Var) (E : Env Var) (M : Term Var)
+    (hd : x ∉ E.dom) (hf : x ∉ E.fv) :
+    psubst (E.update x s).toAssignment M = (psubst E.toAssignment M)[x := s] := by
+  simp only [Env.update_toAssignment]
+  induction M with
+    grind [subst_fresh, Function.update_self, Function.update_of_ne,
+      toAssignment_fresh, toAssignment_not_fvar]
+
+end LambdaCalculus.LocallyNameless.Untyped.Term
+
+end Cslib