User-defined Set simplification rule not applied

On K master commit (72d33ae0e0), the following very simple spec does not work. This affects some KEVM proofs which are being ported.

requires "domains.md"

module TEST
    imports INT
    imports SET

    configuration <k> $PGM:Step </k>

    syntax Step ::= run ( Set ) | done ( Set )

    rule <k> run(S) => done(S) ... </k>

    syntax Bool ::= pred ( Int ) [function, no-evaluators]

    rule .Set -Set _ => .Set [simplification]
    rule (SetItem(X) REST) -Set SetItem(Y) => SetItem(X) (REST -Set SetItem(Y)) requires pred(X) andBool notBool pred(Y) [simplification]

    rule pred(X) => false requires 1 <=Int X andBool X <=Int 9 [simplification]
endmodule

module TEST-SPEC
    imports TEST

    claim <k> run(SetItem(1) -Set SetItem(X)) => done(SetItem(1)) ... </k> requires pred(X)

endmodule

To reproduce the failure:

kompile --backend haskell test.k --main-module TEST --syntax-module TEST
kprove test.k --def-module TEST --spec-module TEST-SPEC

Start by reproducing the failure with kompile --backend haskell test.k --main-module TEST --syntax-module TEST and kprove test.k --def-module TEST --spec-module TEST-SPEC. Inspect how the simplification rules in the TEST module interact with the claim in TEST-SPEC. Done means the provided proof succeeds for the user-defined Set rules.