fix applying big_sepL_singleton
This came up when bumping Iris in LambdaRust.
I am not extremely happy about arbitrarily putting some PM option combinators into cbv and some into cbn, but this produced the best results. The reason is that We do not always want pm_default emp P
to unfold, which is notation involving pm_from_option
.
Alternatively, we could:
- Define (in
bi/derived_connectives.v
) a functionoption PROP -> PROP
that defaults toemp
, use that for lemmas related tobi_wandM
, add that function tocbn
and movepm_from_option
andpm_option_fun
tocbv
. - Generalize
bi_wandM
tobi_wandL
that takes a list, and use big-ops to state the lemmas that are currently stated usingpm_default emp
.