diff --git a/stdpp/gmultiset.v b/stdpp/gmultiset.v index 91ff03c03ea33513b335b9745fcb2e7c151cebea..b72865c8075d5983e9e074fde34a4820b5e57619 100644 --- a/stdpp/gmultiset.v +++ b/stdpp/gmultiset.v @@ -832,10 +832,9 @@ Section map. - by subst. Qed. - Global Instance set_unfold_gmultiset_map - f X (P : A → Prop) y : + Global Instance set_unfold_gmultiset_map f X (P : A → Prop) y : (∀ x, SetUnfoldElemOf x X (P x)) → - SetUnfoldElemOf y (gmultiset_map f X) (∃ x, y = f x ∧ P x). + SetUnfoldElemOf y (gmultiset_map f X) (∃ x, y = f x ∧ P x). Proof. constructor. rewrite elem_of_gmultiset_map; naive_solver. Qed. Global Instance multiset_unfold_map x X n f :