add more option-included lemmas
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).