case nil
α : Type u_1
β : Type ?u.996
L₂ : List (List α)
⊢ join ([] ++ L₂) = join [] ++ join L₂

case cons
α : Type u_1
β : Type ?u.996
L₂ : List (List α)
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : join (tail✝ ++ L₂) = join tail✝ ++ join L₂
⊢ join (head✝ :: tail✝ ++ L₂) = join (head✝ :: tail✝) ++ join L₂
α : Type u_1
β : Type ?u.996
L₁ L₂ : List (List α)
⊢ join (L₁ ++ L₂) = join L₁ ++ join L₂
induction L₁
no goals
case nil
α : Type u_1
β : Type ?u.996
L₂ : List (List α)
⊢ join ([] ++ L₂) = join [] ++ join L₂
rfl
no goals
case cons
α : Type u_1
β : Type ?u.996
L₂ : List (List α)
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : join (tail✝ ++ L₂) = join tail✝ ++ join L₂
⊢ join (head✝ :: tail✝ ++ L₂) = join (head✝ :: tail✝) ++ join L₂
simp [*]