basic): `filter` is a `coframe` (#12872)

Commit

3 years ago

feat(order/filter/basic): `filter` is a `coframe` (#12872) Provide the `coframe (filter α)` instance and remove now duplicated lemmas.

Author

YaelDillies

Parents