∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.WithInitial C)ᵒᵖ),
  (CategoryTheory.WithInitial.opEquiv C).unitIso.inv.app X =
    (match Opposite.unop X with
      | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (Opposite.op (CategoryTheory.WithInitial.of x))
      | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (Opposite.op CategoryTheory.WithInitial.star)).inv