∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.Functor ℕᵒᵖ C}
  (app : (n : ℕ) → F.obj (Opposite.op n) ⟶ G.obj (Opposite.op n))
  (naturality :
    ∀ (n : ℕ),
      CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯).op) (app n) =
        CategoryTheory.CategoryStruct.comp (app (n + 1)) (G.map (CategoryTheory.homOfLE ⋯).op))
  (n : ℕᵒᵖ), (CategoryTheory.NatTrans.ofOpSequence app naturality).app n = app (Opposite.unop n)