Commit d6139cd3 authored by Ralf Jung's avatar Ralf Jung
Browse files

strengthen big_sepS_sepS to bi-entailment

parent 72810c5c
......@@ -2251,7 +2251,7 @@ End gset.
Lemma big_sepS_sepS `{Countable A, Countable B}
(X : gset A) (Y : gset B) (Φ : A B PROP) :
([ set] x X, [ set] y Y, Φ x y) - ([ set] y Y, [ set] x X, Φ x y).
([ set] x X, [ set] y Y, Φ x y) ([ set] y Y, [ set] x X, Φ x y).
Proof.
repeat setoid_rewrite big_sepS_elements.
rewrite big_sepL_sepL. done.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment