Problem with cherry picking function sets

[rodrigo7491]

Description

Another bug discovered via #1588. It seems to be encoding-independent.

Input specification

------ MODULE Oracle --------
VARIABLES
  \* @type: Set((Bool -> Int));
  witness,
  \* @type: Bool;
  found

Init ==
  /\ witness \in {[{TRUE} -> {0, 12}], [{TRUE} -> {13, 1}]}
  /\ found \in BOOLEAN

Next ==
  UNCHANGED <<witness, found>>

NotFound ==
  ~found
======================

The command line parameters used to run the tool

apalache-mc check --smt-encoding=oopsla19 Oracle.tla
apalache-mc check --smt-encoding=arrays Oracle.tla

Additional context

at.forsyte.apalache.tla.bmcmt.RewriterException: Do not know how pick an element from a set of type: FinFunSet[CellTFrom(Set(Bool)), CellTFrom(Set(Int))]

[konnov]

This is related to #1452