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

Add lemma `gmultiset_not_elem_of_empty`.

parent 0120e6fa
No related branches found
No related tags found
1 merge request!251Introduce `SingletonMS` class for multiset singletons.
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 0 deletions
theories/gmultiset.v
+ 2
− 0
View file @ fde7718b
...@@ -370,6 +370,8 @@ Section more_lemmas. ...@@ -370,6 +370,8 @@ Section more_lemmas.
Proof. multiset_solver. Qed. Proof. multiset_solver. Qed.
(** Element of operation *) (** Element of operation *)
Lemma gmultiset_not_elem_of_empty x : x ∉@{gmultiset A} ∅.
Proof. multiset_solver. Qed.
Lemma gmultiset_not_elem_of_singleton x y : x ∉@{gmultiset A} {[+ y +]} ↔ x ≠ y. Lemma gmultiset_not_elem_of_singleton x y : x ∉@{gmultiset A} {[+ y +]} ↔ x ≠ y.
Proof. multiset_solver. Qed. Proof. multiset_solver. Qed.
Lemma gmultiset_not_elem_of_union x X Y : x ∉ X ∪ Y ↔ x ∉ X ∧ x ∉ Y. Lemma gmultiset_not_elem_of_union x X Y : x ∉ X ∪ Y ↔ x ∉ X ∧ x ∉ Y.
......
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