Lemma with an `ensures` clause is not being applied

We are using the following lemma:

rule [keccak-eq-conc-false]: keccak(A)  ==Int B => false
    ensures #notEq(keccak(A), B, "keccak-eq-conc-false") [symbolic(A), concrete(B), simplification, comm]

The idea is that sometimes we want to assume that the keccak of a symbolic expression will not collide with a pre-existing concrete value, but we are using the ensures clause to record this assumption in the configuration (with a new #notEq symbol) so we can check afterwards that the cases where this lemma is applied are sound.

However, we have the following claim:

claim [lookup-keccak]:
    <k> runLemma ( #lookup ( STORAGE:Map [ 1 <- 2 ] , keccak ( X ) ) )
    => doneLemma ( #lookup ( STORAGE:Map , keccak ( X ) ) ) ... </k>

It should be passing by the lemma above and this lemma about #lookup, but it fails with the lemma as it is. However, if we remove the ensures clause, it passes.

I'm attaching a keccak-lemmas.k file with the lemma and claim above. The behavior should be reproducible using kprove. It's worth noting that this claim is based on a proof that we were running with the booster, where this subexpression was also not being simplified.

keccak-lemmas.k.txt

Start with the attached keccak-lemmas.k.txt and reproduce the lookup-keccak claim using kprove. Compare the behavior with and without the ensures clause, then inspect the referenced #lookup lemma in kevm-pyk/kproj/evm-semantics/lemmas/lemmas.k. Done means the claim passes while the ensures clause records the #notEq assumption.