∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] (x : (CategoryTheory.WithTerminal C)ᵒᵖ),
  (match CategoryTheory.CategoryStruct.id x with
    | Opposite.op f =>
      match x, x, f, CategoryTheory.CategoryStruct.id x with
      | Opposite.op (CategoryTheory.WithTerminal.of x), Opposite.op (CategoryTheory.WithTerminal.of y), f, x_1 =>
        (CategoryTheory.WithTerminal.down f).op
      | Opposite.op CategoryTheory.WithTerminal.star, Opposite.op (CategoryTheory.WithTerminal.of a), x, x_1 =>
        CategoryTheory.WithInitial.starInitial.to
          (match Opposite.op (CategoryTheory.WithTerminal.of a) with
          | Opposite.op x =>
            match x with
            | CategoryTheory.WithTerminal.of x => CategoryTheory.WithInitial.of (Opposite.op x)
            | CategoryTheory.WithTerminal.star => CategoryTheory.WithInitial.star)
      | Opposite.op CategoryTheory.WithTerminal.star, Opposite.op CategoryTheory.WithTerminal.star, x, x_1 =>
        CategoryTheory.CategoryStruct.id
          (match Opposite.op CategoryTheory.WithTerminal.star with
          | Opposite.op x =>
            match x with
            | CategoryTheory.WithTerminal.of x => CategoryTheory.WithInitial.of (Opposite.op x)
            | CategoryTheory.WithTerminal.star => CategoryTheory.WithInitial.star)) =
    CategoryTheory.CategoryStruct.id
      (match x with
      | Opposite.op x =>
        match x with
        | CategoryTheory.WithTerminal.of x => CategoryTheory.WithInitial.of (Opposite.op x)
        | CategoryTheory.WithTerminal.star => CategoryTheory.WithInitial.star)