no goals
α : Type u_1
β : Type ?u.238
γ : Type ?u.241
δ : Type ?u.244
l : List α
L : List (List α)
⊢ join ↑(List.map ofList (l :: L)) = ↑(List.join (l :: L))
simp only [join, List.map, coe_sum, List.sum_cons, List.join, ←coe_add, ←coe_join L]