no goals
α : Type u_1
β : Type ?u.8378
γ : Type ?u.8381
M : Type ?u.8384
inst✝¹ : Monoid M
N : Type ?u.8390
inst✝ : Monoid N
xs : List (FreeMonoid α)
⊢ ↑toList (List.prod xs) = List.join (List.map (↑toList) xs)
induction xs <;> simp [*, List.join]