Skip to content
GitLab

Add lemma `later_exist_except_0`.

Merged Robbert Krebbers requested to merge robbert/later_exist_except_0 into master

Making an MR, in case we want to bikeshed about the name.