case nil
α : Type u_1
β : Type ?u.18531
⊢ reverse (join []) = join (reverse (map reverse []))

case cons
α : Type u_1
β : Type ?u.18531
head✝ : List α
tail✝ : List (List α)
ih : reverse (join tail✝) = join (reverse (map reverse tail✝))
⊢ reverse (join (head✝ :: tail✝)) = join (reverse (map reverse (head✝ :: tail✝)))
α : Type u_1
β : Type ?u.18531
L : List (List α)
⊢ reverse (join L) = join (reverse (map reverse L))
induction' L with _ _ ih
no goals
case nil
α : Type u_1
β : Type ?u.18531
⊢ reverse (join []) = join (reverse (map reverse []))
rfl
no goals
case cons
α : Type u_1
β : Type ?u.18531
head✝ : List α
tail✝ : List (List α)
ih : reverse (join tail✝) = join (reverse (map reverse tail✝))
⊢ reverse (join (head✝ :: tail✝)) = join (reverse (map reverse (head✝ :: tail✝)))
rw [join, reverse_append, ih, map_cons, reverse_cons', join_concat]