Skip to content

Strengthen `big_sepL_submseteq` and `big_sep{M,S,MS}_subseteq`

Robbert Krebbers requested to merge robbert/big_subseteq into master

Strengthen big_sepL_submseteq and big_sep{M,S,MS}_subseteq to only require the predicate to be affine, instead of the whole BI.

Merge request reports