diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
new file mode 100644
index 00000000..e4ba4ef2
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
@@ -0,0 +1,309 @@
+import Cslib.Foundations.Data.Relation
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
+
+namespace Cslib
+
+universe u v
+
+namespace LambdaCalculus.LocallyNameless.Stlc
+
+open Untyped Typing LambdaCalculus.LocallyNameless.Untyped.Term
+
+variable {Var : Type u} {Base : Type v} [DecidableEq Var] [HasFresh Var]
+
+open LambdaCalculus.LocallyNameless.Stlc
+open scoped Term
+
+
+
+abbrev Environment (Var : Type u) := Context Var (Term Var)
+
+def multi_subst (σ : Environment Var) (M : Term Var) : Term Var :=
+  match σ with
+  | [] => M
+  | ⟨ i, sub ⟩ :: σ' => (multi_subst σ' M) [ i := sub ]
+
+def fv (Ns : Environment Var) : Finset Var :=
+  match Ns with
+  | [] => {}
+  | ⟨ _, sub ⟩ :: Ns' => sub.fv ∪ fv Ns'
+
+@[simp]
+def context_LC (Γ : Environment Var) : Prop :=
+  ∀ {x M}, ⟨ x, M ⟩ ∈ Γ → LC M
+
+lemma context_LC_cons {Γ : Environment Var} {x : Var} {sub : Term Var} :
+  LC sub → context_LC Γ → context_LC (⟨ x, sub ⟩ :: Γ) := by
+  intro lc_sub lc_Γ y σ h_mem
+  cases h_mem
+  · assumption
+  · apply lc_Γ
+    assumption
+
+
+
+def multi_subst_fvar_fresh (Ns : Environment Var) :
+  ∀ x ∉ Ns.dom, multi_subst Ns (Term.fvar x) = Term.fvar x := by
+  induction Ns <;> intro x h_fresh
+  · case nil =>
+      simp [multi_subst]
+  · case cons N Ns ih =>
+      simp only [multi_subst]
+      simp only [Context.dom] at h_fresh
+      rw[ih]
+      · rw[subst_fvar]
+        by_cases h : N.1 = x <;> simp_all
+      · simp_all
+
+lemma multi_subst_preserves_not_fvar {x : Var}
+  (M : Term Var)
+  (Ns : Environment Var)
+  (nmem : x ∉ M.fv ∪ fv Ns) :
+  x ∉ (multi_subst Ns M).fv := by
+  induction Ns
+  · case nil =>
+      rw[multi_subst]
+      simp_all
+  · case cons N Ns ih =>
+      rw[multi_subst]
+      apply subst_preserve_not_fvar
+      rw[fv] at nmem
+      simp_all
+
+
+
+def multi_subst_app (M N : Term Var) (Ps : Environment Var) :
+        multi_subst Ps (Term.app M N) = Term.app (multi_subst Ps M) (multi_subst Ps N) := by
+  induction Ps
+  · rfl
+  · case cons N Ns ih => rw[multi_subst,multi_subst,ih]; rfl
+
+def multi_subst_abs (M : Term Var) (Ns : Environment Var) :
+    multi_subst Ns (Term.abs M) =
+    Term.abs (multi_subst Ns M) := by
+  induction Ns
+  · rfl
+  · case cons N Ns ih => rw[multi_subst, ih]; rfl
+
+lemma open'_fvar_subst (M N : Term Var) (x : Var) (H : x ∉ Term.fv M) :
+  (i : Nat) → (M ⟦ i ↝ Term.fvar x ⟧) [x := N] = M ⟦ i ↝ N ⟧ := by
+  induction M <;> intro i
+  · case bvar j =>
+      rw[Term.openRec_bvar, Term.openRec_bvar]
+      by_cases h : i = j <;> simp[h, Term.subst_fvar, Term.subst_bvar]
+  · case fvar y =>
+      rw[Term.openRec_fvar, Term.openRec_fvar]
+      simp only [Term.fv, Finset.mem_singleton] at H
+      simp only [subst_fvar, ite_eq_right_iff]
+      intro H
+      contradiction
+  · case abs M ih =>
+      rw[Term.openRec_abs, Term.openRec_abs]
+      rw[Term.subst_abs]
+      rw[ih H]
+  · case app l r ih_l ih_r =>
+      rw[Term.openRec_app, Term.openRec_app]
+      rw[Term.subst_app]
+      simp only [Term.fv, Finset.mem_union, not_or] at H
+      rw[ih_l H.1]
+      rw[ih_r H.2]
+
+
+lemma multi_subst_open_var (M : Term Var) (Ns : Environment Var) (x : Var) :
+  x ∉ Ns.dom →
+  context_LC Ns →
+  (multi_subst Ns (M ^ (Term.fvar x))) =
+  (multi_subst Ns M) ^ (Term.fvar x) := by
+  intro h_ndom h_lc
+  induction Ns with
+  | nil => rfl
+  | cons N Ns ih =>
+    rw[multi_subst, multi_subst]
+    rw[ih]
+    · rw[subst_open_var] <;> aesop
+    · simp_all
+    aesop
+
+inductive saturated (S : Set (Term Var)) : Prop :=
+| intro : (∀ M ∈ S, LC M) →
+          (∀ M ∈ S, SN M) →
+          (∀ M, neutral M → LC M → M ∈ S) →
+          (∀ M N P, LC N → SN N → multi_app (M ^ N) P ∈ S → multi_app ((Term.abs M).app N) P ∈ S) →
+          saturated S
+
+
+@[simp]
+def semanticMap (τ : Ty Base) : Set (Term Var) :=
+  match τ with
+  | Ty.base _ => { t : Term Var | SN t ∧ LC t }
+  | Ty.arrow τ₁ τ₂ =>
+    { t : Term Var | ∀ s : Term Var, s ∈ semanticMap τ₁ → (Term.app t s) ∈ semanticMap τ₂ }
+
+lemma multi_app_lc : ∀ {M P : Term Var} {Ns : List (Term Var)},
+  LC (multi_app M Ns) → (LC M → LC P) → LC (multi_app P Ns) := by
+  intro N P Ns
+  induction Ns <;> intro lc_Ns lc_P
+  · simp_all[multi_app]
+  · case cons a l ih =>
+      rw[multi_app]
+      rw[multi_app] at lc_Ns
+      cases lc_Ns
+      grind
+
+theorem lcAt_openRec_lcAt (M N : Term Var) (i : ℕ) :
+    LcAt i (M⟦i ↝ N⟧) → LcAt (i + 1) M := by
+  induction M generalizing i <;> try grind
+
+lemma open_abs_lc : forall {M N : Term Var},
+  LC (M ^ N) → LC (M.abs) := by
+  intro M N hlc
+  rw[←lcAt_iff_LC]
+  rw[←lcAt_iff_LC] at hlc
+  apply lcAt_openRec_lcAt _ _ _ hlc
+
+
+def semanticMap_saturated (τ : Ty Base) :
+    @saturated Var (semanticMap τ) := by
+  induction τ
+  · case base b =>
+      constructor
+      · simp_all
+      · simp_all
+      · simp_all[neutral_sn]
+      · intro M N P lc_N sn_N h_app
+        constructor
+        · simp_all[multi_app_sn]
+        · apply multi_app_lc
+          · apply h_app.2
+          · intro Hlc
+            constructor
+            · apply open_abs_lc
+              assumption
+            · assumption
+  · case arrow τ₁ τ₂ ih₁ ih₂ =>
+      constructor
+      · intro M hM
+        have H := ih₁.3 (.fvar (fresh {})) (.fvar (fresh {})) (.fvar (fresh {}))
+        specialize (hM (fvar (fresh {})) H)
+        apply (ih₂.1) at hM
+        cases hM
+        assumption
+      · intro M hM
+        apply sn_app_left M (Term.fvar (fresh {}))
+        · constructor
+        · have H := ih₁.3 (.fvar (fresh {})) (.fvar (fresh {})) (.fvar (fresh {}))
+          specialize (hM (fvar (fresh {})) H)
+          apply ih₂.2 ; assumption
+      · intro M hneut mlc s hs
+        apply ih₂.3
+        · constructor
+          · assumption
+          · apply ih₁.2
+            assumption
+        · constructor
+          · assumption
+          · apply ih₁.1
+            assumption
+      · intro M N P lc_N sn_N h_app s hs
+        apply ih₂.4 M N (s::P)
+        · apply lc_N
+        · apply sn_N
+        · apply h_app
+          assumption
+
+
+
+
+
+def entails_context (Ns : Context Var (Term Var)) (Γ : Context Var (Ty Base)) :=
+  ∀ {x τ}, ⟨ x, τ ⟩ ∈ Γ → (multi_subst Ns (Term.fvar x)) ∈ semanticMap τ
+
+lemma entails_context_empty {Γ : Context Var (Ty Base)} :
+  entails_context [] Γ := by
+  intro x τ h_mem
+  rw[multi_subst]
+  apply (semanticMap_saturated τ).3 <;> constructor
+
+
+lemma entails_context_cons (Ns : Context Var (Term Var)) (Γ : Context Var (Ty Base))
+  (x : Var) (τ : Ty Base) (sub : Term Var) :
+  x ∉ Ns.dom ∪ fv Ns ∪ Γ.dom →
+  sub ∈ semanticMap τ →
+  entails_context Ns Γ → entails_context (⟨ x, sub ⟩ :: Ns) (⟨ x, τ ⟩ :: Γ) := by
+  intro h_fresh h_mem h_entails y σ h_mem
+  rw[multi_subst]
+  rw[entails_context] at h_entails
+  cases h_mem
+  · case head =>
+    rw[multi_subst_fvar_fresh]
+    · rw[subst_fvar]
+      simp_all
+    · simp_all
+  · case tail h_mem =>
+    specialize (h_entails h_mem)
+    rw [subst_fresh]
+    · assumption
+    · apply multi_subst_preserves_not_fvar
+      apply List.mem_keys_of_mem at h_mem
+      aesop
+
+
+
+
+def entails (Γ : Context Var (Ty Base)) (t : Term Var) (τ : Ty Base) :=
+  ∀ Ns, context_LC Ns → (entails_context Ns Γ) → (multi_subst Ns t) ∈ semanticMap τ
+
+
+
+
+theorem soundness {Γ : Context Var (Ty Base)} {t : Term Var} {τ : Ty Base} :
+  Γ ⊢ t ∶ τ → entails Γ t τ := by
+  intro derivation_t
+  induction derivation_t
+  · case var Γ xσ_mem_Γ =>
+      intro Ns lc_Ns hsat
+      apply hsat xσ_mem_Γ
+  · case' abs σ Γ t τ L IH derivation_t =>
+      intro Ns lc_Ns hsat s hsat_s
+      rw[multi_subst_abs]
+      apply (semanticMap_saturated _).4 _ _ []
+      · apply (semanticMap_saturated _).1
+        assumption
+      · apply (semanticMap_saturated _).2
+        assumption
+      · rw[multi_app]
+        set x := fresh (t.fv ∪ L ∪ Ns.dom ∪ fv Ns ∪ Context.dom Γ ∪ (multi_subst Ns t).fv)
+        have hfresh : x ∉ t.fv ∪ L ∪ Ns.dom ∪ fv Ns ∪ Context.dom Γ  ∪ (multi_subst Ns t).fv := by apply fresh_notMem
+        have hfreshL : x ∉ L := by simp_all
+        have H1 := derivation_t x hfreshL
+        rw[entails] at H1
+        specialize H1 (⟨x,s⟩ :: Ns)
+        rw [multi_subst, multi_subst_open_var, ←subst_intro] at H1
+        · apply H1
+          · apply context_LC_cons
+            · apply (semanticMap_saturated _).1
+              assumption
+            · assumption
+          · apply entails_context_cons <;> simp_all
+        · simp_all
+        · apply (semanticMap_saturated σ).1
+          assumption
+        · simp_all
+        · aesop
+  · case app derivation_t derivation_t' IH IH' =>
+      intro Ns lc_Ns hsat
+      rw[multi_subst_app]
+      apply IH Ns lc_Ns hsat
+      apply IH' Ns lc_Ns hsat
+
+theorem strong_norm {Γ} {t : Term Var} {τ : Ty Base} (der : Γ ⊢ t ∶ τ) : SN t := by
+  have H := soundness der [] (by aesop) entails_context_empty
+  apply (semanticMap_saturated τ).2
+  assumption
+
+end LambdaCalculus.LocallyNameless.Stlc
+
+end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
index bb0a866c..ed2f614e 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
@@ -55,6 +55,8 @@ lemma step_lc_l (step : M ⭢βᶠ M') : LC M := by
   induction step <;> constructor
   all_goals assumption
 
+
+
 /-- Left congruence rule for application in multiple reduction. -/
 @[scoped grind ←]
 theorem redex_app_l_cong (redex : M ↠βᶠ M') (lc_N : LC N) : app M N ↠βᶠ app M' N := by
@@ -86,6 +88,20 @@ lemma redex_subst_cong (s s' : Term Var) (x y : Var) (step : s ⭢βᶠ s') :
   case abs => grind [abs <| free_union Var]
   all_goals grind
 
+/-- Substitution respects a single reduction step. -/
+lemma redex_subst_cong_lc (s s' t : Term Var) (x : Var) (step : s ⭢βᶠ s') (h_lc : LC t) :
+    s [ x := t ] ⭢βᶠ s' [ x := t ] := by
+  induction step
+  case beta m n abs_lc n_lc =>
+    cases abs_lc with | abs xs _ mem =>
+      rw [subst_open x t n m (by grind)]
+      refine beta ?_ (by grind)
+      exact subst_lc (LC.abs xs m mem) h_lc
+  case abs => grind [abs <| free_union Var]
+  all_goals grind
+
+
+
 /-- Abstracting then closing preserves a single reduction. -/
 lemma step_abs_close {x : Var} (step : M ⭢βᶠ M') : M⟦0 ↜ x⟧.abs ⭢βᶠ M'⟦0 ↜ x⟧.abs := by
   grind [abs ∅, redex_subst_cong]
@@ -97,6 +113,13 @@ lemma redex_abs_close {x : Var} (step : M ↠βᶠ M') : (M⟦0 ↜ x⟧.abs ↠
   case single ih => exact Relation.ReflTransGen.single (step_abs_close ih)
   case trans l r => exact Relation.ReflTransGen.trans l r
 
+/-- Multiple reduction of opening implies multiple reduction of abstraction. -/
+theorem step_abs_cong (xs : Finset Var) (cofin : ∀ x ∉ xs, (M ^ fvar x) ⭢βᶠ (M' ^ fvar x)) :
+    M.abs ⭢βᶠ M'.abs := by
+  have ⟨fresh, _⟩ := fresh_exists <| free_union [fv] Var
+  rw [open_close fresh M 0 ?_, open_close fresh M' 0 ?_]
+  all_goals grind [step_abs_close]
+
 /-- Multiple reduction of opening implies multiple reduction of abstraction. -/
 theorem redex_abs_cong (xs : Finset Var) (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠βᶠ (M' ^ fvar x)) :
     M.abs ↠βᶠ M'.abs := by
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
index f72a8a98..e06e6f87 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
@@ -116,6 +116,7 @@ theorem beta_lc {M N : Term Var} (m_lc : M.abs.LC) (n_lc : LC N) : LC (M ^ N) :=
   cases m_lc with
   | abs => grind [fresh_exists <| free_union [fv] Var]
 
+
 /-- Opening then closing is equivalent to substitution. -/
 @[scoped grind =]
 lemma open_close_to_subst (m : Term Var) (x y : Var) (k : ℕ) (m_lc : LC m) :
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
new file mode 100644
index 00000000..2957f007
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
@@ -0,0 +1,421 @@
+module
+
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
+
+public section
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u}
+
+
+namespace LambdaCalculus.LocallyNameless.Untyped.Term
+
+attribute [grind =] Finset.union_singleton
+
+lemma steps_lc_l [DecidableEq Var] [HasFresh Var] {M M' : Term Var} (steps : M ↠βᶠ M') (lc_M : LC M) : LC M' := by
+  induction steps <;> grind[FullBeta.step_lc_r]
+
+lemma steps_lc [DecidableEq Var] [HasFresh Var]
+  {M M' : Term Var} (steps : M ↠βᶠ M') (lc_M : LC M) : LC M' := by
+  induction steps <;> grind[FullBeta.step_lc_r]
+
+lemma steps_lc_or_rfl [HasFresh Var] [DecidableEq Var] {M M' : Term Var} :
+  M ↠βᶠ M' →
+  LC M' ∨ M = M' := by
+  intro redex
+  cases redex <;> grind[FullBeta.step_lc_r]
+
+@[simp]
+def multi_app (f : Term Var) (args : List (Term Var)) :=
+  match args with
+  | []      => f
+  | a :: as => Term.app (multi_app f as) a
+
+
+@[reduction_sys "βᶠ"]
+inductive multi_app_full_beta : List (Term Var) → List (Term Var) → Prop where
+| step : N ⭢βᶠ N' → (∀ N ∈ Ns, LC N) → multi_app_full_beta (N :: Ns) (N' :: Ns)
+| cons : LC N → multi_app_full_beta Ns Ns' → multi_app_full_beta (N :: Ns) (N :: Ns')
+
+
+
+lemma multi_app_step_lc_r [DecidableEq Var] [HasFresh Var]
+  {Ns Ns' : List (Term Var)} (step : Ns ⭢βᶠ Ns') : (∀ N ∈ Ns', LC N) := by
+  induction step <;> grind[FullBeta.step_lc_r]
+
+lemma multi_app_steps_lc [DecidableEq Var] [HasFresh Var]
+  {Ns Ns' : List (Term Var)} (step : Ns ↠βᶠ Ns') (H : ∀ N ∈ Ns, LC N) : (∀ N ∈ Ns', LC N) := by
+  induction step <;> grind[FullBeta.step_lc_r, multi_app_step_lc_r]
+
+
+@[scoped grind ←]
+lemma multi_app_lc {M : Term Var} {Ns : List (Term Var)} :
+  LC (M.multi_app Ns) ↔
+  LC M ∧
+  (∀ N ∈ Ns, LC N)
+   := by
+  constructor
+  · induction Ns
+    · case nil => grind[multi_app]
+    · case cons N Ns ih =>
+        intro h_lc
+        cases h_lc
+        grind
+  · induction Ns <;> grind[multi_app, LC.app]
+
+@[scoped grind ←]
+lemma step_multi_app_l {M M' : Term Var} {Ns : List (Term Var)} :
+  M ⭢βᶠ M' →
+  (∀ N ∈ Ns, LC N) →
+  M.multi_app Ns ⭢βᶠ M'.multi_app Ns := by
+  induction Ns <;> grind[multi_app, FullBeta.appR]
+
+@[scoped grind ←]
+lemma step_multi_app_r {M : Term Var} {Ns Ns' : List (Term Var)} :
+  Ns ⭢βᶠ Ns' →
+  LC M →
+  M.multi_app Ns ⭢βᶠ M.multi_app Ns' := by
+  intro Ns_red; induction Ns_red <;> grind[multi_app,FullBeta.appL,FullBeta.appR]
+
+
+
+@[scoped grind ←]
+lemma steps_multi_app_l {M M' : Term Var} {Ns : List (Term Var)} :
+  M ↠βᶠ M' →
+  (∀ N ∈ Ns, LC N) →
+  M.multi_app Ns ↠βᶠ M'.multi_app Ns := by
+  intro redex
+  induction redex <;> grind
+
+@[scoped grind ←]
+lemma steps_multi_app_r {M : Term Var} {Ns Ns' : List (Term Var)} :
+  Ns ↠βᶠ Ns' →
+  LC M →
+  M.multi_app Ns ↠βᶠ M.multi_app Ns' := by
+  intro Ns_red; induction Ns_red <;> grind[multi_app,FullBeta.appL,FullBeta.appR]
+
+
+lemma invert_multi_app_st [DecidableEq Var] [HasFresh Var] : ∀ {Ps} {M N Q : Term Var},
+  multi_app (M.abs.app N) Ps ⭢βᶠ Q →
+  (∃ M', M.abs ⭢βᶠ Term.abs M' ∧ Q = multi_app (M'.abs.app N) Ps) ∨
+  (∃ N', N ⭢βᶠ N' ∧ Q = multi_app (M.abs.app N') Ps) ∨
+  (∃ Ps', Ps ⭢βᶠ Ps' ∧ Q = multi_app (M.abs.app N) Ps') ∨
+  (Q = multi_app (M ^ N) Ps) := by
+  intro Ps
+  induction Ps with
+  | nil =>
+    intro N N P h_red
+    rw[multi_app] at h_red
+    rw[multi_app]
+    cases h_red
+    · case beta abs_lc n_lc => aesop
+    · case appL M N' lc_z h_red => aesop
+    · case appR M M' lc_z h_red =>
+        left
+        cases lc_z
+        · case abs M' xs h_lc =>
+            exists M'
+            constructor
+            · apply FullBeta.step_abs_cong
+              assumption
+            · rfl
+  | cons P Ps ih =>
+    intro M N Q h_red
+    have h_lc := (FullBeta.step_lc_l h_red)
+    rw [multi_app] at h_red
+    generalize Heq : (M.abs.app N).multi_app Ps = Q'
+    rw[Heq] at h_red
+    cases h_red
+    · case beta abs_lc n_lc => cases Ps <;> contradiction
+    · case appL Y M P' lc_z h_red =>
+        right
+        right
+        left
+        exists (P' :: Ps)
+        constructor
+        · constructor
+          · assumption
+          · rw[multi_app_lc] at h_lc
+            simp_all
+        · aesop
+    · case appR M Q'' h_red P_lc =>
+        rw[←Heq] at h_red
+        match (ih h_red) with
+        | .inl ⟨ M', st, Heq' ⟩ => aesop
+        | .inr (.inl ⟨ N', st, Heq' ⟩) => aesop
+        | .inr (.inr (.inl ⟨ Ps', st, Heq' ⟩)) =>
+          right
+          right
+          left
+          exists (P :: Ps')
+          constructor
+          · constructor <;> assumption
+          · aesop
+        | .inr (.inr (.inr Heq')) => aesop
+
+lemma invert_multi_app_mst [DecidableEq Var] [HasFresh Var] : ∀ {Ps} {M N Q : Term Var},
+  multi_app (M.abs.app N) Ps ↠βᶠ Q →
+  ∃ M' N' Ns', M.abs ↠βᶠ M'.abs ∧ N ↠βᶠ N' ∧ Ps ↠βᶠ Ns' ∧
+    (Q = multi_app (M'.abs.app N') Ns' ∨
+     (multi_app (M.abs.app N) Ps ↠βᶠ multi_app (M'^ N') Ns' ∧
+                                      multi_app (M'^ N') Ns' ↠βᶠ Q)) := by
+  intro Ps M N Q h_red
+  induction h_red
+  · case refl => grind
+  · case tail Q' Q'' steps step ih =>
+    match ih with
+    | ⟨ M', N', Ps', st_M, st_N, st_Ps, Cases ⟩ =>
+      match Cases with
+      | .inl Heq =>
+        rw[Heq] at step
+        match (invert_multi_app_st step) with
+        | .inl ⟨ M'', st, HeqM'' ⟩ => grind
+        | .inr (.inl ⟨ N', st, Heq' ⟩) => grind
+        | .inr (.inr (.inl ⟨ Ps', st, Heq' ⟩)) => grind
+        | .inr (.inr (.inr Heq')) => grind
+      | .inr ⟨ steps1, steps2 ⟩ =>
+        exists M', N', Ps'
+        constructor
+        · assumption
+        · constructor
+          · assumption
+          · constructor
+            · assumption
+            · right
+              constructor
+              · assumption
+              · transitivity
+                · assumption
+                · apply Relation.ReflTransGen.single
+                  assumption
+
+
+
+inductive SN {α} : Term α → Prop
+| sn t : (∀ (t' : Term α), (t ⭢βᶠ t') → SN t') → SN t
+
+@[aesop safe]
+lemma sn_step {t t' : Term Var} (t_st_t' : t ⭢βᶠ t') (sn_t : SN t) : SN t' := by
+  cases sn_t; grind
+
+@[aesop safe]
+lemma sn_mst {t t' : Term Var} (t_st_t' : t ↠βᶠ t') (sn_t : SN t) : SN t' := by
+  induction t_st_t' <;> grind[sn_step]
+
+lemma sn_fvar {x : Var} : SN (Term.fvar x) := by
+  constructor
+  intro t' hstep
+  cases hstep
+
+lemma sn_app (t s : Term Var) :
+  SN t →
+  SN s →
+  (∀ {t' s' : Term Var}, t ↠βᶠ t'.abs → s ↠βᶠ s' → SN (t' ^ s')) →
+  SN (t.app s) := by
+  intro h_sn_t h_sn_s hβ
+  induction h_sn_t generalizing s with | sn t ht ih_t =>
+  induction h_sn_s with | sn s hs ih_s =>
+  constructor
+  intro u hstep
+  cases hstep with
+  | beta _ _ => apply hβ <;> rfl
+  | appL _ h_s_red =>
+    apply ih_s _ h_s_red
+    intro t' s'' hstep1 hstep2
+    exact hβ hstep1 (Relation.ReflTransGen.head h_s_red hstep2)
+  | appR _ h_t_red =>
+    apply ih_t _ h_t_red _ (SN.sn s hs)
+    intro t' s' hstep1 hstep2
+    exact hβ (Relation.ReflTransGen.head h_t_red hstep1) hstep2
+
+
+
+lemma sn_app_left (M N : Term Var) : Term.LC N → SN (M.app N) → SN M := by
+  intro lc_N h_sn
+  generalize Heq : M.app N = P
+  rw[Heq] at h_sn
+  revert M N
+  induction h_sn
+  · case sn P h_sn ih =>
+    intro M N lc_N Heq
+    rw[←Heq] at ih
+    constructor
+    intro M' h_step
+    apply ih (M'.app N)
+    apply Term.FullBeta.appR <;> assumption
+    · assumption
+    · rfl
+
+lemma sn_app_right (M N : Term Var) : Term.LC M → SN (M.app N) → SN N := by
+  intro lc_N h_sn
+  generalize Heq : M.app N = P
+  rw[Heq] at h_sn
+  revert M N
+  induction h_sn
+  · case sn P h_sn ih =>
+    intro M N lc_N Heq
+    rw[←Heq] at ih
+    constructor
+    intro N' h_step
+    apply ih (M.app N')
+    apply Term.FullBeta.appL <;> assumption
+    · assumption
+    · rfl
+
+@[aesop safe constructors]
+inductive neutral : Term Var → Prop
+| bvar : ∀ n, neutral (Term.bvar n)
+| fvar : ∀ x, neutral (Term.fvar x)
+| app : ∀ t1 t2, neutral t1 → SN t2 → neutral (Term.app t1 t2)
+
+@[aesop safe]
+lemma neutral_step {t : Term Var} :
+  neutral t → ∀ t', t ⭢βᶠ t' → neutral t' := by
+  intro Hneut
+  induction Hneut <;> intro t' step
+  · case bvar n =>
+      cases step
+  · case fvar x =>
+      cases step
+  · case app IH Hneut =>
+      cases step <;> try aesop
+      · contradiction
+      constructor
+      · assumption
+      · apply sn_step <;> assumption
+
+@[aesop safe]
+lemma neutral_mst {t t' : Term Var} :
+  neutral t → t ↠βᶠ t' → neutral t' := by
+  intro Hneut h_red
+  induction h_red <;> aesop
+
+lemma neutral_sn {t : Term Var} (Hneut : neutral t) : SN t := by
+  induction Hneut
+  · case bvar n => constructor; intro t' hstep; cases hstep
+  · case fvar x => constructor; intro t' hstep; cases hstep
+  · case app t1 t'_neut t1_sn t1'_sn =>
+      apply sn_app <;> try assumption
+      intro t1' t2' hstep1 hstep2
+      have H_neut := neutral_mst t'_neut hstep1
+      contradiction
+
+lemma redex_open_cong_lc (s s' t : Term Var) (step : s.abs ⭢βᶠ s'.abs) (h_lc : LC t) :
+    (s ^ t) ⭢βᶠ (s' ^ t) := by sorry
+
+lemma abs_sn : ∀ {M N : Term Var},
+  SN (M ^ N)  → SN (Term.abs M) := by
+  intro M N sn_M
+  generalize h : (M ^ N) = M_open at sn_M
+  revert N M
+  induction sn_M with
+  | sn M_open h_sn ih =>
+      intro M N h
+      constructor
+      intro M' h_step
+      cases h_step with
+      | @abs h_M_red M' L H =>
+        specialize ih (M' ^ N)
+        rw[←h] at ih
+        apply ih
+        · apply redex_open_cong_lc <;> try assumption
+          · sorry
+          · sorry
+        · rfl
+
+/-- Substitution respects a single reduction step. -/
+lemma redex_subst_cong_lc (s s' t : Term Var) (x : Var) (step : s ⭢βᶠ s') (h_lc : LC t) :
+    s [ x := t ] ⭢βᶠ s' [ x := t ] := by
+  induction step
+  case beta m n abs_lc n_lc =>
+    cases abs_lc with | abs xs _ mem =>
+      rw [subst_open x t n m (by grind)]
+      refine beta ?_ (by grind)
+      exact subst_lc (LC.abs xs m mem) h_lc
+  case abs => grind [abs <| free_union Var]
+  all_goals grind
+
+
+lemma step_open [DecidableEq Var] [HasFresh Var] : ∀ {M M' N : Term Var},
+  LC N →
+  M.abs ⭢βᶠ M'.abs →
+  (M ^ N) ⭢βᶠ (M' ^ N) := by
+  intro M M' N lc_N h_step
+  cases h_step
+  · case abs L h_step =>
+      let x := fresh (L ∪ M.fv ∪ M'.fv ∪ N.fv)
+      have x_fresh : x ∉ L ∪ M.fv ∪ M'.fv ∪ N.fv := by apply fresh_notMem
+      specialize h_step x (by simp_all)
+      rw[subst_intro x _ M (by simp_all) lc_N]
+      rw[subst_intro x _ M' (by simp_all) lc_N]
+      apply FullBeta.redex_subst_cong_lc
+      · assumption
+      assumption
+
+
+
+
+lemma redex_open_cong_lc' (s s' t t' : Term Var) (step1 : t ↠βᶠ t') (step2 : s.abs ↠βᶠ s'.abs) (h_lc : LC t) :
+    (s ^ t) ↠βᶠ (s' ^ t') := by sorry
+
+lemma multi_app_sn [DecidableEq Var] [HasFresh Var] : ∀ {Ps} {M N : Term Var},
+  SN N →
+  SN (multi_app (M ^ N) Ps) →
+  LC (multi_app (M ^ N) Ps) →
+  -------------------------------------
+  SN (multi_app ((Term.abs M).app N) Ps) := by
+  intro P
+  induction P <;> intros M N sn_N sn_MNPs lc_MNPs
+  · case nil =>
+      apply sn_app
+      · apply abs_sn at sn_MNPs
+        assumption
+      · assumption
+      · intro M' N' hstep1 hstep2
+        rw[multi_app] at sn_MNPs
+        have Hmst : (M ^ N) ↠βᶠ (M' ^ N') := by
+          apply redex_open_cong_lc' <;>  try assumption
+          · sorry
+        apply sn_mst <;> assumption
+  · case cons P Ps ih =>
+      apply sn_app
+      · apply ih
+        · assumption
+        · apply sn_app_left at sn_MNPs <;> grind[multi_app_lc]
+        · grind[multi_app_lc]
+      · apply sn_app_right at sn_MNPs
+        · assumption
+        · cases lc_MNPs
+          assumption
+      · intro Q' P' hstep1 hstep2
+        match (invert_multi_app_mst hstep1) with
+        | ⟨ M', N', Ps', h_M_red, h_N_red, h_Ps_red, h_cases ⟩ =>
+          match h_cases with
+          | Or.inl h_P => cases Ps' <;> rw[multi_app] at h_cases <;> contradiction
+          | Or.inr ⟨ h_st1, h_st2 ⟩ =>
+            have H1 : (multi_app (M ^ N) Ps).app P ↠βᶠ Q' ^ P' := by
+              have H2 : (multi_app (M ^ N) Ps) ↠βᶠ (M' ^ N').multi_app Ps' := by
+                transitivity
+                · apply steps_multi_app_r
+                  · assumption
+                  · rw[multi_app_lc] at lc_MNPs
+                    simp_all
+                · apply steps_multi_app_l
+                  · apply redex_open_cong_lc' <;> try assumption
+                    · sorry
+                  · rw[multi_app_lc] at lc_MNPs
+                    apply multi_app_steps_lc at h_Ps_red
+                    simp_all
+              have H3 : (multi_app (M ^ N) Ps) ↠βᶠ Q'.abs := by
+                transitivity <;> try assumption
+              have H4 : Q'.abs.app P' ↠βᶠ Q' ^ P' := by grind[FullBeta.beta, steps_lc_l]
+              have H4 : ((M ^ N).multi_app Ps).app P ↠βᶠ Q'.abs.app P' := by
+                cases lc_MNPs
+                transitivity
+                · apply FullBeta.redex_app_r_cong <;> assumption
+                · apply FullBeta.redex_app_l_cong <;> grind[steps_lc_l]
+              transitivity <;> try assumption
+            apply sn_mst <;> try assumption