Cannot apply rule for symbolic list with multiple elements

Symbolic list unification fails with multiple elements

To reproduce:

tmp.k:

module TMP
  imports INT
  imports LIST

  syntax KItem ::= "push" | "pop"
  syntax KItem ::= Int

  rule  <k> push => .K ... </k>
        <stack> (.List => ListItem(1)) ... </stack>

  rule  <k> pop => .K ... </k>
        <stack> (ListItem(_:KItem) => .List) ... </stack>
    [label(xyzzy)]

  configuration
    <T>
      <k color="green"> .K </k>
      <stack> .List </stack>
    </T>

endmodule

tmp-proof.k:

module TMP-PROOF
  imports TMP

  claim 
      <T>
        <k> push ~> push ~> pop ~> pop ~> K:K </k>
        <stack> Stack:List </stack>
      </T>
      =>
      <T>
        <k> K </k>
        <stack> Stack </stack>
      </T>
endmodule

to run:

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

The repl provides no reason explaining why the xyzzy rule is not applied:

Kore (0)> step 2
Kore (2)> try xyzzy
No explanation given
Kore (2)> 

Note that the claim above works with a single push/pop, i.e. <k> push ~> pop ~> K:K </k>

Start with the tmp.k symbolic list rules and tmp-proof.k claim, then reproduce the failure with kompile tmp.k --backend haskell && kprove tmp-proof.k. Inspect the REPL behavior for try xyzzy after the two pushes; done means the multiple-element case is handled and the REPL no longer reports no explanation for the failed application.