∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{u_1, u_2} D] {S : D} {T : CategoryTheory.Functor C D}
  {f f' : CategoryTheory.StructuredArrow S T} (g : f.right ⟶ f'.right),
  CategoryTheory.CategoryStruct.comp f.hom (T.map g) = f'.hom →
    CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.fromPUnit S).map (CategoryTheory.CategoryStruct.id f.left)) f'.hom =
      CategoryTheory.CategoryStruct.comp f.hom (T.map g)