From e7405db5495b46186912a7a1a6be1cb08c87b281 Mon Sep 17 00:00:00 2001 From: Marijn van Wezel <marijn@wikibase.nl> Date: Thu, 17 Oct 2024 15:37:43 +0200 Subject: [PATCH] Improve styling --- stdpp/gmultiset.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/stdpp/gmultiset.v b/stdpp/gmultiset.v index 91ff03c0..b72865c8 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 : -- GitLab