Usimplified <non-empty-user-list> #Equals <empty-user-list>

For a user-defined list, the backend produces an unsimplified predicate that can be described as <list-element> .UserList #Equals .UserList. I think that the backend should simplify this to #Bottom.

To reproduce:

1. Unpack the attached archive.
2. kore-exec haskellDefinition.bin --module ELROND-WASM --pattern program.kore --output result.kore --depth 2
3. result.kore contains this:

    /* Sfa */
    \not{SortGeneratedTopCell{}}(
        /* Spa */
        \equals{SortK{}, SortGeneratedTopCell{}}(
            /* T Fn D Sfa */
            kseq{}(
                /* T Fn D Sfa */
                /* Inj: */ inj{SortStmts{}, SortKItem{}}(
                    /* T Fn D Sfa */
                    Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(
                        /* T Fn D Sfa Cl */
                        LblnewEmptyModule'UndsUnds'WASM-AUTO-ALLOCATE'Unds'Stmt'Unds'WasmString{}(
                            /* T Fn D Sfa Cli */
                            /* Inj: */ inj{SortWasmStringToken{}, SortWasmString{}}(
                                /* T Fn D Sfa Cl */
                                \dv{SortWasmStringToken{}}(/* T Fn D Sfa Cl */
                                "\"env\"")
                            )
                        ),
                        /* T Fn D Sfa Cli */
                        /* Inj: */ inj{SortEmptyStmts{}, SortStmts{}}(
                            /* T Fn D Sfa Cl */
                            Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}()
                        )
                    )
                ),
                /* T Fn D Sfa Cl */ dotk{}()
            ),
            /* T Fn D Sfa Cl */
            kseq{}(
                /* T Fn D Sfa Cli */
                /* Inj: */ inj{SortEmptyStmts{}, SortKItem{}}(
                    /* T Fn D Sfa Cl */
                    Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}()
                ),
                /* T Fn D Sfa Cl */ dotk{}()
            )
        )
    )

unsimplified.zip

Start by unpacking unsimplified.zip and running the kore-exec command with haskellDefinition.bin, the ELROND-WASM module, and program.kore pattern. Inspect result.kore for the user-list equality predicate; done means the unsimplified predicate is reduced to #Bottom.