diff --git a/prelude/logic.lp b/prelude/logic.lp
index 856bce41fd9fb5a94e7815aaf9f040cf20974fee..66947840b33eb5d1aec1fef8e0f2a3b407cdb6dd 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -87,7 +87,6 @@ proof
 admit
 
 constant symbol reflexivity_of_equals: Prf (∀B (λt, ∀ (λx: El t, x = x)))
-set builtin "refl" ≔ reflexivity_of_equals
 
 constant
 symbol transitivity_of_equals