From 2cbe4b4f2eb9ba426bf9c1650eb9fbfdb5dabf2d Mon Sep 17 00:00:00 2001
From: Marijn van Wezel <marijn@wikibase.nl>
Date: Thu, 17 Oct 2024 15:36:56 +0200
Subject: [PATCH] Slightly simplify proof
---
stdpp/gmultiset.v | 5 ++---
1 file changed, 2 insertions(+), 3 deletions(-)
diff --git a/stdpp/gmultiset.v b/stdpp/gmultiset.v
index 7ed96a54..91ff03c0 100644
--- a/stdpp/gmultiset.v
+++ b/stdpp/gmultiset.v
@@ -818,9 +818,8 @@ Section map.
Proof.
induction X as [|x' X IH] using gmultiset_ind; intros Hinj.
- multiset_solver.
- - rewrite gmultiset_map_disj_union, !multiplicity_disj_union, IH; [|done].
- destruct (bool_decide (x = x'));
- rewrite gmultiset_map_singleton; multiset_solver.
+ - rewrite gmultiset_map_disj_union, gmultiset_map_singleton, !multiplicity_disj_union.
+ destruct (bool_decide (x = x')); multiset_solver.
Qed.
Lemma gmultiset_map_eq_iff f X Y :
--
GitLab