removed refl builtin from prelude

85250f99 · hondet · e60d3b0c · 85250f99
Commit 85250f99 authored 4 years ago by hondet
--- 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