Add lemmas about empty `filter` on list, map, and set

Added an advanced lemma about [filter] on lists. Whenever a filter with a proposition [P] on a list [l] results in an empty list, we can derive that x ∉ l for any [x] where P x.