Skip to content
Snippets Groups Projects
Commit 661f6dfc authored by Ralf Jung's avatar Ralf Jung
Browse files

fix a typo

parent fa8d6908
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 1 deletion
theories/collections.v
+ 1
− 1
View file @ 661f6dfc
...@@ -63,7 +63,7 @@ Section simple_collection. ...@@ -63,7 +63,7 @@ Section simple_collection.
Global Instance elem_of_proper : Global Instance elem_of_proper :
Proper ((=) ==> (≡) ==> iff) (@elem_of A C _) | 5. Proper ((=) ==> (≡) ==> iff) (@elem_of A C _) | 5.
Proof. intros ???; subst. firstorder. Qed. Proof. intros ???; subst. firstorder. Qed.
Global Instance disjoint_prope : Proper ((≡) ==> (≡) ==> iff) (@disjoint C _). Global Instance disjoint_proper: Proper ((≡) ==> (≡) ==> iff) (@disjoint C _).
Proof. intros ??????. by rewrite !elem_of_disjoint; setoid_subst. Qed. Proof. intros ??????. by rewrite !elem_of_disjoint; setoid_subst. Qed.
Lemma elem_of_union_list Xs x : x ∈ ⋃ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X. Lemma elem_of_union_list Xs x : x ∈ ⋃ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X.
Proof. Proof.
......
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