Skip to content
Snippets Groups Projects
Commit 91ea2bfa authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix inconsistent arguments of `subset_difference_elem_of`.

parent 59911631
No related branches found
No related tags found
No related merge requests found
......@@ -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.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment