A or B can be something else other than true or false

To reproduce: tmp.tar.gz

tmp.k:

module TMP
  imports BOOL
  imports INT

  syntax KItem ::= split(Bool)

  rule split(true) => .K
  rule split(false) => .K

  syntax A ::= a(Int)
endmodule

proof-tmp.k:

module PROOF-TMP
  imports TMP

  imports K-EQUAL-SYNTAX
  imports MAP

  claim split(a(X) ==K a(Y) orBool a(X) in_keys(M:Map)) => .K
endmodule

command line:

kompile tmp.k --backend haskell && kprove proof-tmp.k

Relevant part of the output:

kore-exec: [380566] Warning (WarnStuckClaimState):
    (InfoReachability) while checking the implication:
    The claim cannot be rewritten further, and the claimed implication is not valid. /mnt/data/runtime-verification/elrond-multisig/tmp/proof-tmp.k:7:9-7:62
  #Not ( #Not ( {
      X
    #Equals
      Y
    } )
  #And
    {
      false
    #Equals
      a ( X ) in_keys ( M )
    } )
#And
  #Not ( {
    true
  #Equals
    ( a ( X ) ~> . ) ==K ( a ( Y ) ~> . ) orBool ( a ( X ) in_keys ( M ) )
  } )
#And
  <k>
    split ( ( a ( X ) ~> . ) ==K ( a ( Y ) ~> . ) orBool ( a ( X ) in_keys ( M ) ) ) ~> _DotVar1 ~> .
  </k>

Info for myself: The original proof is protocol-correctness/proof/malicious-user/can-be-deleted/run-external-call-from-user/proof-recfu-discard-action-void.k at commit 96e3cd486c33bfbc3473664d7a5533614524ff76.

Reproduce the issue using tmp.k and proof-tmp.k with kompile tmp.k --backend haskell && kprove proof-tmp.k, then inspect the kore-exec WarnStuckClaimState output. Compare this minimal case with the original proof at protocol-correctness/proof/malicious-user/can-be-deleted/run-external-call-from-user/proof-recfu-discard-action-void.k and the referenced commit. Done means the claim no longer gets stuck because the Boolean expression is treated as only true or false.