diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
index e4eb25e3e5..f0ccb55611 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
@@ -86,15 +86,9 @@ module LEMMAS [symbolic]
   // Map Reasoning
   // ########################
 
-    rule keys(.Map)             => .Set                    [simplification]
-    rule keys(M [ K <- _V ])    => keys(M) |Set SetItem(K) [simplification]
-    rule keys(M [ K <- undef ]) => keys(M) -Set SetItem(K) [simplification]
-
     rule 0 <=Int #lookup( _M:Map , _ )             => true [simplification, smt-lemma]
     rule         #lookup( _M:Map , _ ) <Int pow256 => true [simplification, smt-lemma]
 
-    rule #lookup(M:Map, X:Int) => 0 requires notBool (X:Int in keys(M):Set) [simplification]
-
     rule #lookup ( _M:Map [ K1 <- V1 ] , K2 )    => #lookup ( K1 |-> V1 , K1 ) requires K1 ==Int  K2 [simplification]
     rule #lookup (  M:Map [ K1 <- _  ] , K2 )    => #lookup ( M         , K2 ) requires K1 =/=Int K2 [simplification]
     rule #lookup ( (K1:Int |-> _) M:Map, K2:Int) => #lookup ( M,          K2 ) requires K1 =/=Int K2 [simplification]