Quantification over sequences

[Zixian Cai <fzcz...@xxxxxxxxx>]

Hi,

I’m just wondering whether it is possible to have quantification over non-numerals.
For example, I would like to say, \E lst \in Seq(1..n): … or \E lst \in Seq(Nat): …

When I check it using TLC, it says “TLC encountered a non-enumerable quantifier bound”.

Sincerely,
Zixian