rw [h_inds]
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss :
  joinF.associatorLeft asss ≫ joinF.associatorRight asss =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor asss)
ass : List (List α)
h_indss :
  joinF.associatorLeft (ass :: asss) ≫ joinF.associatorRight (ass :: asss) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor (ass :: asss))
a : α
as : List α
h_inds :
  joinF.associatorLeft ((as :: ass) :: asss) ≫ joinF.associatorRight ((as :: ass) :: asss) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))
⊢ DVect2.cons (𝟙 a) (joinF.associatorLeft ((as :: ass) :: asss) ≫ joinF.associatorRight ((as :: ass) :: asss)) =
    DVect2.cons (𝟙 a)
      (𝟙
        (as ++ Prefunctor.obj joinF.toPrefunctor ass ++
          Prefunctor.obj joinF.toPrefunctor
            (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF).toPrefunctor asss)))
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss :
  joinF.associatorLeft asss ≫ joinF.associatorRight asss =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor asss)
ass : List (List α)
h_indss :
  joinF.associatorLeft (ass :: asss) ≫ joinF.associatorRight (ass :: asss) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor (ass :: asss))
a : α
as : List α
h_inds :
  joinF.associatorLeft ((as :: ass) :: asss) ≫ joinF.associatorRight ((as :: ass) :: asss) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))
⊢ DVect2.cons (𝟙 a)
      (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))) =
    DVect2.cons (𝟙 a)
      (𝟙
        (as ++ Prefunctor.obj joinF.toPrefunctor ass ++
          Prefunctor.obj joinF.toPrefunctor
            (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF).toPrefunctor asss)))