Commit cc9683cb authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'robbert/subset_difference_elem_of' into 'master'

Fix inconsistent arguments of `subset_difference_elem_of`.

See merge request !252
parents c6aa1f5f 91ea2bfa
Pipeline #45285 passed with stage
in 9 minutes and 32 seconds
......@@ -677,7 +677,7 @@ Section set.
Proof. set_solver. Qed.
Lemma difference_disjoint X Y : X ## Y X Y X.
Proof. set_solver. Qed.
Lemma subset_difference_elem_of {x: A} {s: C} (inx: x s): s {[ x ]} s.
Lemma subset_difference_elem_of x X : x X X {[ x ]} X.
Proof. set_solver. Qed.
Lemma difference_difference X Y Z : (X Y) Z X (Y Z).
Proof. set_solver. Qed.
Markdown is supported
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