Skip to content
Snippets Groups Projects

Fix inconsistent arguments of `subset_difference_elem_of`.

Merged Fix inconsistent arguments of `subset_difference_elem_of`.
robbert/subset_difference_elem_of into master
Merged Robbert Krebbers requested to merge robbert/subset_difference_elem_of into master
Compare
and
1 file
+ 1
− 1
Compare changes
  • Side-by-side
  • Inline
theories/sets.v
+ 1
− 1
@@ -677,7 +677,7 @@ Section set.
@@ -677,7 +677,7 @@ Section set.
Proof. set_solver. Qed.
Proof. set_solver. Qed.
Lemma difference_disjoint X Y : X ## Y → X ∖ Y ≡ X.
Lemma difference_disjoint X Y : X ## Y → X ∖ Y ≡ X.
Proof. set_solver. Qed.
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.
Proof. set_solver. Qed.
Lemma difference_difference X Y Z : (X ∖ Y) ∖ Z ≡ X ∖ (Y ∪ Z).
Lemma difference_difference X Y Z : (X ∖ Y) ∖ Z ≡ X ∖ (Y ∪ Z).
Proof. set_solver. Qed.
Proof. set_solver. Qed.