diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 3246c3d80..74afb01ea 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -197,7 +197,7 @@ end = struct
 
   let _Tt = Tt
   let _Ff = Ff
-  let _Eq x y = Eq (x, y)
+  let _Eq x y = if equal_trm x y then Tt else Eq (x, y)
   let _Dq x y = Dq (x, y)
   let _Eq0 x = Eq0 x