∀ {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] (F : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D)
  (x : C),
  CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.incl.obj x)))
      (CategoryTheory.Iso.refl (F.obj CategoryTheory.WithTerminal.star)).hom =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.incl.comp F)).hom.app x)
      ((fun x => F.map (CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.of x))) x)