Skip to content
Snippets Groups Projects
Unverified Commit 2cbe4b4f authored by Marijn van Wezel's avatar Marijn van Wezel
Browse files

Slightly simplify proof

parent 3f7421c7
No related branches found
No related tags found
1 merge request!577Add `gmultiset_map` and associated lemmas
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 3 deletions
stdpp/gmultiset.v
+ 2
− 3
View file @ 2cbe4b4f
......@@ -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 :
......
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