Skip to content

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

Jonas Kastberg requested to merge jihgfee/stdpp:filter_lemmas into master

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.

Edited by Robbert Krebbers

Merge request reports