case h.h
α : Type u_1
l : List (List α)
⊢ join l = joinTR l
⊢ @join = @joinTR
funext α l
case h.h
α : Type u_1
l : List (List α)
⊢ bindTR l id = joinTR l
case h.h
α : Type u_1
l : List (List α)
⊢ join l = joinTR l
rw [← List.bind_id, List.bind_eq_bindTR]
no goals
case h.h
α : Type u_1
l : List (List α)
⊢ bindTR l id = joinTR l
rfl