∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) {F F' : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
  (f : F ⟶ F') (x : F.obj (Opposite.op X)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.yonedaEquiv.symm x) f =
    CategoryTheory.yonedaEquiv.symm (f.app (Opposite.op X) x)