Cannot simplify proof dealing with indirect equalities

I have a module where I want to assert things about a Map in the pre-condition, and use that knowledge to check a post condition. Attached is the generated bug report. This example comes from porting the benchmark proofs of KEVM over to the Haskell backend. Here is the K definition:

module TEST
    imports DOMAINS

    configuration
        <k> $PGM:Foo </k>
        <mem> .Map </mem>

    syntax Foo ::= doIt ( Int , Int )
    rule <k> doIt(K, V) => . ... </k>
         <mem> M => M [ K <- V +Int #lookup(M, K) ] </mem>

    syntax Int ::= #lookup ( Map , Int ) [function, functional, smtlib(lookup)]
 // ---------------------------------------------------------------------------
    rule #lookup( (KEY |-> VAL:Int) _M , KEY ) => VAL modInt 256
    rule #lookup(                    M , KEY ) => 0              requires notBool KEY in_keys(M)
    rule #lookup( (KEY |-> VAL    ) _M , KEY ) => 0              requires notBool isInt(VAL)

endmodule

And the specification module:

requires "test.k"
 
module TEST-SPEC
    imports TEST

    rule <k> doIt(K, V1) => . ... </k>
         <mem> S => S [ K <- ?V3 ] </mem>
      requires 0 <=Int V1 andBool V1 <Int 256
       andBool #lookup(S, K) ==Int V2
       andBool 0 <=Int V2 andBool V2 <Int 256
       andBool 0 <=Int V2 +Int V1 andBool V2 +Int V1 <Int 256

       ensures ?V3 ==Int V2 +Int V1
endmodule

In the output counterexample, I get this clause in the side-condition (i):

  #Not ( #Exists ?V3 . {
      ?V3 ==Int V2 +Int V1
    #Equals
      true
    }
  #And
    {
      S [ K:Int <- V1 +Int #lookup ( S , K ) ]
    #Equals
      S [ K:Int <- ?V3:Int ]
    } )

But we also have in the path condition (ii):

  {
    true
  #Equals
    #lookup ( S , K ) ==Int V2
  }

So it should be able to simplify (i) using (ii) to see that it's infeasible, and prune this branch, is my thinking.

Here is the generated bug report: test.tar.gz

Start with the attached test.tar.gz bug report and the TEST and TEST-SPEC definitions, then inspect the generated counterexample's side-condition (i) alongside path condition (ii). Reproduce the indirect-equality case and determine whether simplification can use the #lookup equality to prune the branch; done means the infeasible branch is simplified away.