Commit 6d2e61e1 by Robbert Krebbers

### Turn unused disjoint_union_difference into something more sensible.

parent f81b0ff3
 ... @@ -418,7 +418,7 @@ Section collection. ... @@ -418,7 +418,7 @@ Section collection. Proof. set_solver. Qed. Proof. set_solver. Qed. Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z. Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z. Proof. set_solver. Qed. Proof. set_solver. Qed. Lemma disjoint_union_difference X Y : X ⊥ Y → (X ∪ Y) ∖ X ≡ Y. Lemma difference_disjoint X Y : X ⊥ Y → X ∖ Y ≡ X. Proof. set_solver. Qed. Proof. set_solver. Qed. Section leibniz. Section leibniz. ... @@ -438,8 +438,8 @@ Section collection. ... @@ -438,8 +438,8 @@ Section collection. Lemma difference_intersection_distr_l_L X Y Z : Lemma difference_intersection_distr_l_L X Y Z : (X ∩ Y) ∖ Z = X ∖ Z ∩ Y ∖ Z. (X ∩ Y) ∖ Z = X ∖ Z ∩ Y ∖ Z. Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed. Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed. Lemma disjoint_union_difference_L X Y : X ⊥ Y → (X ∪ Y) ∖ X = Y. Lemma difference_disjoint_L X Y : X ⊥ Y → X ∖ Y = X. Proof. unfold_leibniz. apply disjoint_union_difference. Qed. Proof. unfold_leibniz. apply difference_disjoint. Qed. End leibniz. End leibniz. Section dec. Section dec. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!