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).