proposition: Lemma gmultiset_ind (P : gmultiset A → Prop) : P ∅ → (∀ x X, P X → P ({[+ x +]} ⊎ X)) → ∀ X, P X.
proof: Proof. intros Hemp Hinsert X. induction (gmultiset_wf X) as [X _ IH]. destruct (gmultiset_choose_or_empty X) as [[x Hx]| ->]; auto. rewrite (gmultiset_disj_union_difference' x X) by done. apply Hinsert, IH; multiset_solver. Qed.
imports: stdpp(gmap) stdpp(options)