diff --git a/src/language/term/Equality.re b/src/language/term/Equality.re
index 1911f51d7e..c87f18f348 100644
--- a/src/language/term/Equality.re
+++ b/src/language/term/Equality.re
@@ -163,11 +163,19 @@ let equality =
           // Both variables are free, so we first check ctxs, and then use the free_var_handler if provided.
           let lookup1 = {
             let* env1 = env1;
-            Environment.lookup(env1, x);
+            let v = Environment.lookup(env1, x);
+            switch (v) {
+            | Some({term: Var(v), _}) when v == x => None
+            | _ => v
+            };
           };
           let lookup2 = {
             let* env2 = env2;
-            Environment.lookup(env2, y);
+            let v = Environment.lookup(env2, y);
+            switch (v) {
+            | Some({term: Var(v), _}) when v == y => None
+            | _ => v
+            };
           };
           switch (lookup1, lookup2) {
           | (Some(v1), Some(v2)) => exp'(v1, v2)