Skip to content

add more option-included lemmas

Ralf Jung requested to merge ralf/some-included-refl into master

The Some_included_refl basically complement Some_included_mono as the two ways to "construct" a Some a ≼ Some b.

Some_valid_included is a version of cmra_valid_included, because applying cmra_valid_included when you have Some a ≼ Some b around is rather frustrating (mostly because Coq lacks good tactics for that kind of forward reasoning).

Edited by Ralf Jung

Merge request reports