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

Shorten proof of `singleton_union_difference`.

parent 7fdaea0f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 4 deletions
theories/sets.v
+ 1
− 4
View file @ dd04c27a
...@@ -795,10 +795,7 @@ Section set. ...@@ -795,10 +795,7 @@ Section set.
Proof. set_solver. Qed. Proof. set_solver. Qed.
Lemma singleton_union_difference X Y x : Lemma singleton_union_difference X Y x :
{[x]} ∪ (X ∖ Y) ≡ ({[x]} ∪ X) ∖ (Y ∖ {[x]}). {[x]} ∪ (X ∖ Y) ≡ ({[x]} ∪ X) ∖ (Y ∖ {[x]}).
Proof. Proof. intro y; destruct (decide (y ∈@{C} {[x]})); set_solver. Qed.
intro y; split; intros Hy; [ set_solver | ].
destruct (decide (y ∈ ({[x]} : C))); set_solver.
Qed.
Context `{!LeibnizEquiv C}. Context `{!LeibnizEquiv C}.
Lemma union_difference_L X Y : X ⊆ Y → Y = X ∪ Y ∖ X. Lemma union_difference_L X Y : X ⊆ Y → Y = X ∪ Y ∖ X.
......
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