range subset vs forall mem

Stream: general

[Yury G. Kudryashov]

Should we prefer range f ⊆ s or ∀ x, f x ∈ s? The first version is better if we have a simp lemma about range f. The other lemma can be directly applied to x.