Commit 2020-01-16 10:23 58610ffd

chore(order/filter/*): use s ∈ f instead of s ∈ f.sets (#1885) Other changes:

• compose old mem_infi and mem_binfi with mem_Union and mem_bUnion_iff to avoid .sets and simplify usage (it was rw [mem_infi, mem_Union] every time)
• drop lift_sets_eq and mem_lift_iff in favor of mem_lift_sets