Commit 2021-09-01 12:16 faf5e5c9

feat(order/bounded_lattice): unbot and untop (#8885) unbot sends non-⊥ elements of with_bot α to the corresponding element of α. untop does the analogous thing for with_top.