From 9fd4210712eff0c54bd5fc5d4acf865ab0bd5876 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 23 Mar 2016 17:51:59 +0100 Subject: [PATCH] fix a typo --- prelude/collections.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prelude/collections.v b/prelude/collections.v index 51f5ec485..e7c050cca 100644 --- a/prelude/collections.v +++ b/prelude/collections.v @@ -63,7 +63,7 @@ Section simple_collection. Global Instance elem_of_proper : Proper ((=) ==> (≡) ==> iff) (@elem_of A C _) | 5. 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. Lemma elem_of_union_list Xs x : x ∈ ⋃ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X. Proof. -- GitLab