∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : (CategoryTheory.WithInitial C)ᵒᵖ) → (Opposite.unop y ⟶ Opposite.unop x) → (x ⟶ y) → Sort u_3)
  (x :
    Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
      Opposite.unop (Opposite.op CategoryTheory.WithInitial.star))
  (x_1 : Opposite.op CategoryTheory.WithInitial.star ⟶ Opposite.op CategoryTheory.WithInitial.star)
  (h_1 :
    (x y : C) →
      (f :
          Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of y)) ⟶
            Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of x))) →
        (x_2 : Opposite.op (CategoryTheory.WithInitial.of x) ⟶ Opposite.op (CategoryTheory.WithInitial.of y)) →
          motive (Opposite.op (CategoryTheory.WithInitial.of x)) (Opposite.op (CategoryTheory.WithInitial.of y)) f x_2)
  (h_2 :
    (a : C) →
      (x :
          Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
            Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of a))) →
        (x_2 : Opposite.op (CategoryTheory.WithInitial.of a) ⟶ Opposite.op CategoryTheory.WithInitial.star) →
          motive (Opposite.op (CategoryTheory.WithInitial.of a)) (Opposite.op CategoryTheory.WithInitial.star) x x_2)
  (h_3 :
    (x :
        Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
          Opposite.unop (Opposite.op CategoryTheory.WithInitial.star)) →
      (x_2 : Opposite.op CategoryTheory.WithInitial.star ⟶ Opposite.op CategoryTheory.WithInitial.star) →
        motive (Opposite.op CategoryTheory.WithInitial.star) (Opposite.op CategoryTheory.WithInitial.star) x x_2),
  (match Opposite.op CategoryTheory.WithInitial.star, Opposite.op CategoryTheory.WithInitial.star, x, x_1 with
    | Opposite.op (CategoryTheory.WithInitial.of x), Opposite.op (CategoryTheory.WithInitial.of y), f, x_2 =>
      h_1 x y f x_2
    | Opposite.op (CategoryTheory.WithInitial.of a), Opposite.op CategoryTheory.WithInitial.star, x, x_2 => h_2 a x x_2
    | Opposite.op CategoryTheory.WithInitial.star, Opposite.op CategoryTheory.WithInitial.star, x, x_2 => h_3 x x_2) =
    h_3 x x_1