dsimp [appendF.naturatorLax]
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
gs : as₂ ⟶ bs₂
⊢ (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor DVect2.nil ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F [] bs₂ =
    appendF.naturatorLax F [] as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.nil ++ gs)
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
gs : as₂ ⟶ bs₂
⊢ (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor DVect2.nil ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor bs₂) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as₂) ≫
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.nil ++ gs)