refactor(data/list/basic,...): more explicit args (#4866)
This makes the `p` in most lemmas involving the following functions explicit, following the usual explicitness conventions:
- `list.filter`,
- `list.countp`,
- `list.take_while`,
- `multiset.filter`,
- `multiset.countp`,
- `finset.filter`
