Commit 2023-07-13 09:29 e7b874fd
View on Github →feat: add cancel lemmas in WithTop (#5837)
This PR adds four lemmas that allow cancelling addition in WithTop α when the term being cancelled is not ⊤. They complement the existing le/lt versions.