Some lemmas about lists involving sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Split out from
data.list.basic to reduce its dependencies.
If each element of a list can be lifted to some type, then the whole list can be lifted to this