∀ {J : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} J] (j₁ j₂ : J)
  (hj₁ : CategoryTheory.ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁) (l : List J),
  (j₁ :: l).getLast ⋯ = j₂ →
    ∀ (hf : ∀ a ∈ l, CategoryTheory.Zigzag a j₂),
      ({ obj := j₁, property := hj₁ } :: List.pmap (fun x h => { obj := x, property := ⋯ }) l hf).getLast ⋯ =
        { obj := j₂, property := ⋯ }