Add generalized implication lemma for sets, etc.
!697 (merged) adds stronger variants of big_sepM_impl
. Similar variants probably make sense for some of the other big ops and these should be added.
For sets @jung suggested:
Lemma big_sepS_impl_strong `{Countable K} Φ (Ψ : K → PROP) X1 X2 :
([∗ set] x ∈ X1, Φ k x) -∗
□ (∀ (x : X),
⌜x ∈ X2⌝ →
((⌜x ∈ X1⌝ ∧ Φ x) ∨ <affinely> ⌜x ¬∈ X1⌝) -∗
Ψ x) -∗
([∗ set] y ∈ X2, Ψ y) ∗
([∗ set] x ∈ X1∖X2, Φ x).