α : Type u_1
β : Type ?u.314731
γ : Type ?u.314734
σ : Type ?u.314737
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
l : List (List α)
⊢ List.foldr (fun b s => b ++ s) [] l = List.join l
α : Type u_1
β : Type ?u.314731
γ : Type ?u.314734
σ : Type ?u.314737
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
l : List (List α)
⊢ List.foldr (fun b s => (fun x x_1 => x ++ x_1) (l, b, s).snd.fst (l, b, s).snd.snd) [] (id l) = List.join l
dsimp
no goals
α : Type u_1
β : Type ?u.314731
γ : Type ?u.314734
σ : Type ?u.314737
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
l : List (List α)
⊢ List.foldr (fun b s => b ++ s) [] l = List.join l
induction l <;> simp [*]