Commit d4e3d4da authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Added parentheses for clarity, and explicitly named used variable

parent 73c373c1
Pipeline #68949 passed with stage
in 11 minutes and 58 seconds
......@@ -808,8 +808,10 @@ Section set.
intros x. rewrite !elem_of_union; rewrite elem_of_difference.
split; [ | destruct (decide (x Y)) ]; intuition.
Qed.
Lemma difference_difference_union X Y Z : Z X -> X (Y Z) X Y Z.
Proof. rewrite set_equiv. intros. destruct (decide (x Z)); set_solver. Qed.
Lemma difference_difference_union X Y Z : Z X -> X (Y Z) (X Y) Z.
Proof.
rewrite set_equiv. intros ? x. destruct (decide (x Z)); set_solver.
Qed.
Lemma subseteq_disjoint_union X Y : X Y Z, Y X Z X ## Z.
Proof.
......@@ -840,7 +842,8 @@ Section set.
Lemma singleton_union_difference_L X Y x :
{[x]} (X Y) = ({[x]} X) (Y {[x]}).
Proof. unfold_leibniz. apply singleton_union_difference. Qed.
Lemma difference_difference_union_L X Y Z : Z X -> X (Y Z) = X Y Z.
Lemma difference_difference_union_L X Y Z :
Z X -> X (Y Z) = (X Y) Z.
Proof. unfold_leibniz. apply difference_difference_union. Qed.
End dec.
......
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