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.

added 2 commits

• 34945717 - Shorten proof and make lemma name consistent.
• 0e3ba050 - Add similar filter lemmas for maps and sets.

Compare with previous version

Thanks for the MR. I tweaked the lemma statement and proof. I also added similar lemmas for sets and maps.

@jung Can you review?

added 2 commits

• 34945717 - Shorten proof and make lemma name consistent.
• 0e3ba050 - Add similar filter lemmas for maps and sets.

Compare with previous version

changed title from Added a useful lemma about [filter] on list to Add lemmas about {+empty +}filter{++} on list, map, and set

resolved all threads

merged

mentioned in commit ff11f3b2

Merging. Thanks.

mentioned in merge request !394 (merged)