have : ∀ (as bs : List α), (mapF.obj F).obj (as++bs) = (mapF.obj F).obj as ++ (mapF.obj F).obj bs :=
  λ as bs => List.map_append F.obj _ _
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as : List α
ass : List (List α)
h_ind :
  Prefunctor.obj joinF.toPrefunctor
      (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (Prefunctor.obj joinF.toPrefunctor ass)
⊢ Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as ++
      Prefunctor.obj joinF.toPrefunctor
        (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as ++ Prefunctor.obj joinF.toPrefunctor ass)
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as : List α
ass : List (List α)
h_ind :
  Prefunctor.obj joinF.toPrefunctor
      (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (Prefunctor.obj joinF.toPrefunctor ass)
this :
  ∀ (as bs : List α),
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as ++ bs) =
      Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as ++
        Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor bs
⊢ Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as ++
      Prefunctor.obj joinF.toPrefunctor
        (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as ++ Prefunctor.obj joinF.toPrefunctor ass)