no goals
α : Type u_1
s t : Multiset (Multiset α)
⊢ Sections (0 + t) = bind (Sections 0) fun m => map ((fun x x_1 => x + x_1) m) (Sections t)
simp
no goals
α : Type u_1
s✝ t : Multiset (Multiset α)
a : Multiset α
s : Multiset (Multiset α)
ih : Sections (s + t) = bind (Sections s) fun m => map ((fun x x_1 => x + x_1) m) (Sections t)
⊢ Sections (a ::ₘ s + t) = bind (Sections (a ::ₘ s)) fun m => map ((fun x x_1 => x + x_1) m) (Sections t)
simp [ih, bind_assoc, map_bind, bind_map]