diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Simpset.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Simpset.hs
index 0a7e3578de..97c4c07e72 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Simpset.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Simpset.hs
@@ -50,5 +50,4 @@ excludedNames =
   , "PEq"
   , "PCmp"
   , "PSignedCmp"
-  , "ecEq"
   ]
diff --git a/examples/aes/aes.saw b/examples/aes/aes.saw
index 2c4d01c835..45800f2de4 100644
--- a/examples/aes/aes.saw
+++ b/examples/aes/aes.saw
@@ -69,15 +69,14 @@ dec_enc <-
                         decrypt_lemma]
               (cryptol_ss()));
     unfolding ["AESRound", "AESInvRound", "AESFinalRound", "AESFinalInvRound"];
-    simplify (add_cryptol_defs ["ecEq"]
-             (add_prelude_eqs ["bvEq_refl"]
+    simplify (add_prelude_eqs ["bvEq_refl"]
              (addsimps [msgToState_stateToMsg,
                         AddRoundKey_cancel,
                         InvShiftRows_ShiftRows,
                         InvSubBytes_SubBytes,
                         InvMixColumns_MixColumns,
                         stateToMsg_msgToState]
-              (cryptol_ss()))));
+              (cryptol_ss())));
     trivial;
   }
   {{ \msg key -> aesDecrypt (aesEncrypt (msg, key), key) == msg }});
@@ -116,15 +115,14 @@ enc_dec <-
                         decrypt_lemma]
               (cryptol_ss()));
     unfolding ["AESRound", "AESInvRound", "AESFinalRound", "AESFinalInvRound"];
-    simplify (add_cryptol_defs ["ecEq"]
-             (add_prelude_eqs ["bvEq_refl"]
+    simplify (add_prelude_eqs ["bvEq_refl"]
              (addsimps [msgToState_stateToMsg,
                         AddRoundKey_cancel,
                         ShiftRows_InvShiftRows,
                         SubBytes_InvSubBytes,
                         MixColumns_InvMixColumns,
                         stateToMsg_msgToState]
-              (cryptol_ss()))));
+              (cryptol_ss())));
     trivial;
   }
   {{ \msg key -> aesEncrypt (aesDecrypt (msg, key), key) == msg }});