. intros; exact List.join_join _
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a : List (List (List α))), List.join (List.join a) = List.join (List.map List.join a)

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List (List (List α))) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.join f)) (DVect2.join (DVect2.map List.join List.join (fun {a b} ↦ DVect2.join) f))
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List (List (List α))) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.join f)) (DVect2.join (DVect2.map List.join List.join (fun {a b} ↦ DVect2.join) f))