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 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
.