diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
index 3ed77b4c..936ad3eb 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
@@ -8,6 +8,7 @@ module
 
 public import Cslib.Foundations.Data.Relation
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
 
 public section
 
@@ -55,6 +56,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
@@ -74,6 +77,9 @@ lemma step_lc_r (step : M ⭢βᶠ M') : LC M' := by
   case' abs => constructor; assumption
   all_goals grind
 
+lemma steps_lc_or_rfl {M M' : Term Var} (redex : M ↠βᶠ M') : (LC M ∧ LC M') ∨ M = M' := by
+  grind
+
 /-- Substitution respects a single reduction step. -/
 lemma redex_subst_cong (s s' : Term Var) (x y : Var) (step : s ⭢βᶠ s') :
     s [ x := fvar y ] ⭢βᶠ s' [ x := fvar y ] := by
@@ -86,6 +92,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 with
+  | beta => grind [subst_open, beta]
+  | abs  => grind [abs <| free_union Var]
+  | _ => 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 +117,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
@@ -104,6 +131,73 @@ theorem redex_abs_cong (xs : Finset Var) (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠
   rw [open_close fresh M 0 ?_, open_close fresh M' 0 ?_]
   all_goals grind [redex_abs_close]
 
+theorem redex_abs_fvar_finset_exists (xs : Finset Var)
+  (M M' : Term Var)
+  (step : M.abs ⭢βᶠ M'.abs) :
+  ∃ (L : Finset Var), ∀ x ∉ L, (M ^ fvar x) ⭢βᶠ (M' ^ fvar x) := by
+  cases step
+  case abs L cofin => exists L
+
+
+lemma step_open_cong
+  (s s' t) (L : Finset Var) (step : ∀ x ∉ L, (s ^ fvar x) ⭢βᶠ (s' ^ fvar x)) (h_lc : LC t) :
+    (s ^ t) ⭢βᶠ (s' ^ t) := by
+  have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
+  grind [subst_intro, redex_subst_cong_lc]
+
+lemma invert_steps_abs {s t : Term Var} (step : s.abs ↠βᶠ t) :
+    ∃ (s' : Term Var), s.abs ↠βᶠ s'.abs ∧ t = s'.abs := by
+  induction step with
+  | refl => grind
+  | tail _ step _ => cases step with grind [step_abs_cong (free_union Var)]
+
+
+
+lemma steps_open_l_abs
+  (s s' t : Term Var) (steps : s.abs ↠βᶠ s'.abs) (lc_s : LC s.abs) (lc_t : LC t) :
+    (s ^ t) ↠βᶠ (s' ^ t) := by
+  generalize eq : s.abs = s_abs at steps
+  generalize eq' : s'.abs = s'_abs at steps
+  induction steps generalizing s s' with
+  | refl => grind
+  | tail _ step ih =>
+    specialize ih s
+    cases step with grind [invert_steps_abs, step_open_cong (L := free_union Var)]
+
+lemma step_subst_r {x : Var} (s t t' : Term Var) (step : t ⭢βᶠ t') (h_lc : LC s) :
+    (s [ x := t ]) ↠βᶠ (s [ x := t' ]) := by
+  induction h_lc with
+  | fvar y => grind
+  | abs => grind [redex_abs_cong (free_union Var)]
+  | @app l r =>
+     calc
+       (l.app r)[x:=t] ↠βᶠ l[x := t].app (r[x:=t']) := by grind
+       _               ↠βᶠ (l.app r)[x:=t'] := by grind
+
+lemma steps_subst_cong2 {x : Var} (s t t' : Term Var) (step : t ↠βᶠ t') (h_lc : LC s) :
+    (s [ x := t ]) ↠βᶠ (s [ x := t' ]) := by
+  induction step
+  · case refl => rfl
+  · case tail t' t'' steps step ih =>
+    transitivity
+    · apply ih
+    · apply step_subst_r <;> assumption
+
+lemma steps_open_cong_abs (s s' t t' : Term Var)
+    (step1 : t ↠βᶠ t')
+    (step2 : s.abs ↠βᶠ s'.abs)
+    (lc_t : LC t)
+    (lc_s : LC s.abs) :
+    (s ^ t) ↠βᶠ (s' ^ t') := by
+    cases lc_s with
+    | abs L h_lc =>
+      have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
+      rw [subst_intro x t s, subst_intro x t' s']
+      · trans (s ^ fvar x)[x:=t']
+        · grind [steps_subst_cong2]
+        · grind [=_ subst_intro, steps_open_l_abs]
+      all_goals grind
+
 end LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta
 
 end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
index 33b1ba69..fb9770f8 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
@@ -86,4 +86,15 @@ theorem lcAt_iff_LC (M : Term Var) [HasFresh Var] : LcAt 0 M ↔ M.LC := by
         grind [fresh_exists L]
     | _ => grind [cases LC]
 
+theorem lcAt_openRec_lcAt (M N : Term Var) (i : ℕ) :
+    LcAt i (M⟦i ↝ N⟧) → LcAt (i + 1) M := by
+  induction M generalizing i <;> grind
+
+lemma open_abs_lc [HasFresh Var] : 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
+
 end Cslib.LambdaCalculus.LocallyNameless.Untyped.Term