From 2af1692bf4c63c4b85ab3edfe317305fd0403b30 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 3 Nov 2024 17:13:14 -0800
Subject: [PATCH] Remove symeq

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 src/Bergamot/Rules.elm | 4 ----
 1 file changed, 4 deletions(-)

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)