∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) (X : F.Elementsᵒᵖ),
  (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj F).inv.app X =
    CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.unop X).1)