More efficient evaluation of SequencesExt!BoundedSeq when e.g. checking refinement

The module Foo models a system where -at every step- the log is extended by a subsequence of up to length C from the set S. It is straightforward to see that the module Bar refines Foo. However, TLC fails to verify the refinement because it cannot enumerate the set of all subsequences SeqOf(S, 42).

----- MODULE Foo ------
EXTENDS Naturals, Sequences, SequencesExt

CONSTANT S, C

VARIABLE log

Init ==
    log = <<>>

Next ==
    \E suffix \in SeqOf(S, C) :
        log' = log \o suffix

NextRefine ==
    /\ log' \in Seq(S)
    /\ IsPrefix(log, log')
    /\ Len(log') <= Len(log) + C

Spec == Init /\ [][Next]_log
=====

----- MODULE Bar -----
EXTENDS Sequences

VARIABLE log

Spec == log = <<>> /\ [][log' = log \o <<"a">>]_log

Foo == INSTANCE Foo WITH C <- 42, S <- {"a"}
THEOREM Spec => Foo!Spec

\* .cfg files do not accept the ! in Foo!NextRefine
FooNextRefine == Foo!NextRefine
=====

Clearly, when verifying refinement, it's conceptually unnecessary for TLC to enumerate SeqOf(S, 42). Instead, it would be sufficient to check something like NextRefine, which TLC will check if we redefine Next with NextRefine:

CONSTANT Next <- [Foo]FooNextRefine

However, SeqOf could be enhanced to symbolically check ... \in SeqOf(S, C), similar to how TLC checks Seq(S):

https://github.com/tlaplus/tlaplus/blob/475477653f01447f60603288a2785df1447bdbeb/tlatools/org.lamport.tlatools/src/tlc2/module/Sequences.java#L391-L411

Additionally, this new tlc2.value.impl.Value implementation should properly implement tlc2.value.impl.Enumerable#elements to lazily enumerate the elements of SeqOf when evaluating the existential quantification\E s \in SeqOf(S,C): log' = ....

Start with tlc2/module/Sequences.java around the linked Seq(S) membership implementation, then inspect tlc2.value.impl.Value and Enumerable#elements. Implement symbolic membership for SeqOf(S,C) without enumerating all sequences, while preserving lazy element enumeration for existential quantification over SeqOf; verify the refinement example no longer requires exhaustive enumeration.