diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean
index d1e4543a4..d3a1aa1c8 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean
@@ -41,6 +41,7 @@ inductive Term (Var : Type u)
 | abs  : Term Var → Term Var
 /-- Function application. -/
 | app  : Term Var → Term Var → Term Var
+deriving DecidableEq
 
 namespace Term