∀ {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]
  {c c' :
    CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.Functor C D)) (CategoryTheory.Functor.const C)}
  (φ : c ⟶ c') (a : C) (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.WithTerminal.ofCommaObject c).map x)
      (match CategoryTheory.WithTerminal.star with
      | CategoryTheory.WithTerminal.of x => φ.left.app x
      | CategoryTheory.WithTerminal.star => φ.right) =
    CategoryTheory.CategoryStruct.comp
      (match CategoryTheory.WithTerminal.of a with
      | CategoryTheory.WithTerminal.of x => φ.left.app x
      | CategoryTheory.WithTerminal.star => φ.right)
      ((CategoryTheory.WithTerminal.ofCommaObject c').map x)