Skip to content

Add lemma `later_exist_except_0`.

Robbert Krebbers requested to merge robbert/later_exist_except_0 into master

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

Merge request reports