Theorem: Multiset.get_singleton (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
a : α
⊢ get {a} = some a
Tactic:
simp [Multiset.get]
State after:
no goals