diff --git a/Cslib.lean b/Cslib.lean
index 1b7b4c4b1..b504973c3 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -116,6 +116,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEtaConfluence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEta.lean
new file mode 100644
index 000000000..0973c61f8
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEta.lean
@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2026 Maximiliano Onofre Martínez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Maximiliano Onofre Martínez
+-/
+
+module
+
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence
+
+/-! # βη-Confluence for the λ-calculus
+
+## Reference
+
+* [T. Nipkow, *More Church-Rosser Proofs (in Isabelle/HOL)*][Nipkow2001]
+
+-/
+
+@[expose] public section
+
+set_option linter.unusedDecidableInType false
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u}
+
+namespace LambdaCalculus.LocallyNameless.Untyped.Term
+
+open Relation
+
+/-- Full βη-reduction. -/
+@[reduction_sys "βηᶠ"]
+abbrev FullBetaEta : Term Var → Term Var → Prop := FullBeta ⊔ FullEta
+
+namespace FullBetaEta
+
+theorem redex_app_l_cong (redex : M ↠βηᶠ M') (lc_N : LC N) : app M N ↠βηᶠ app M' N := by
+induction redex with
+| refl => grind
+| tail _ h ih =>  apply Relation.ReflTransGen.trans ih
+                  apply Relation.ReflTransGen.single
+                  cases h
+                  · left
+                    apply Xi.appR <;> grind
+                  · right
+                    apply Xi.appR <;> grind
+
+theorem redex_app_r_cong (redex : M ↠βηᶠ M') (lc_N : LC N) : app N M ↠βηᶠ app N M' := by
+induction redex with
+| refl => grind
+| tail _ h ih =>  apply Relation.ReflTransGen.trans ih
+                  apply Relation.ReflTransGen.single
+                  cases h
+                  · left
+                    apply Xi.appL <;> grind
+                  · right
+                    apply Xi.appL <;> grind
+
+end FullBetaEta
+
+end LambdaCalculus.LocallyNameless.Untyped.Term
+
+end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean
index 24ae1c943..d56359e8a 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean
@@ -8,6 +8,7 @@ module
 
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEta
 
 /-! # βη-Confluence for the λ-calculus
 
@@ -32,10 +33,6 @@ namespace LambdaCalculus.LocallyNameless.Untyped.Term
 
 open Relation
 
-/-- Full βη-reduction. -/
-@[reduction_sys "βηᶠ"]
-abbrev FullBetaEta : Term Var → Term Var → Prop := FullBeta ⊔ FullEta
-
 open FullEta FullBeta in
 /-- η-reduction and β-reduction strongly commute. -/
 lemma stronglyCommute_eta_beta : StronglyCommute (@FullEta Var) FullBeta := by