Theorem: HFSet.ofMultiset_cons (Hfzfa.lean)

State before:
atoms : Type u_1
s : Multiset (HFSet atoms)
x : HFSet atoms
⊢ ofMultiset (x ::ₘ s) = insert x (ofMultiset s)
Tactic:
simp [ofMultiset]
State after:
no goals