∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v))
  (X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda F),
  (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ F).inv.app X =
    CategoryTheory.CategoryStruct.id X.left