diff --git a/src/Bergamot/Rules.elm b/src/Bergamot/Rules.elm
index 8bd211a..3ecd222 100644
--- a/src/Bergamot/Rules.elm
+++ b/src/Bergamot/Rules.elm
@@ -206,10 +206,6 @@ builtinRules t =
                     case mp of
                         Nothing -> pure <| MkProofTree { name = "BuiltinNot", conclusion = t, premises = [] }
                         Just _ -> fail)
-            Call "symeq" [Call s1 [], Call s2 []] ->
-                if s1 == s2
-                then pure <| MkProofTree { name = "BuiltinSymEq", conclusion = t, premises = [] }
-                else fail
             _ -> fail
 
 provePremises : List (Term UnificationVar) -> Prover (List ProofTree)