[STATEMENT]
lemma mset_insert: "mset_tree(insert x t) = {#x#} + mset_tree t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_tree (insert x t) = {#x#} + mset_tree t
[PROOF STEP]
by(induction t arbitrary: x) (auto simp: ac_simps)