∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (obj : Fin (n + 1) → C)
  (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ) (i : ℕ)
  (hi : autoParam (i < n) CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_map_succ._auto_1),
  (CategoryTheory.ComposableArrows.mkOfObjOfMapSucc obj mapSucc).map' i (i + 1) ⋯ hi = mapSucc ⟨i, hi⟩