[Move-prover] Allow "in" and subranges in predicates, not just for quantifiers

[DavidLDill]

🚀 Feature Request

We allow expressions like forall i in 0..len(v) ... and forall x in v...

It would be nice to be able to use these in predicates as well. E.g.
forall i in 0..a: f(i) in 0..b
(shorter than 0 <= f(i) && f(i) < b)

and
forall x in v1: x in v2 (subset)

Motivation

Is your feature request related to a problem? Please describe.

Pitch

Describe the solution you'd like

Describe alternatives you've considered

Are you willing to open a pull request? (See CONTRIBUTING)

Additional context