∀ {J : Type u_1} (motive : (x y : CategoryTheory.Limits.WalkingParallelFamily J) → (x ⟶ y) → Sort u_2) (j : J)
  (h_1 :
    (x : CategoryTheory.Limits.WalkingParallelFamily J) →
      motive x x (CategoryTheory.Limits.WalkingParallelFamily.Hom.id x))
  (h_2 :
    (j : J) →
      motive CategoryTheory.Limits.WalkingParallelFamily.zero CategoryTheory.Limits.WalkingParallelFamily.one
        (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)),
  (match CategoryTheory.Limits.WalkingParallelFamily.zero, CategoryTheory.Limits.WalkingParallelFamily.one,
      CategoryTheory.Limits.WalkingParallelFamily.Hom.line j with
    | x, .(x), CategoryTheory.Limits.WalkingParallelFamily.Hom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingParallelFamily.zero), .(CategoryTheory.Limits.WalkingParallelFamily.one),
      CategoryTheory.Limits.WalkingParallelFamily.Hom.line j => h_2 j) =
    h_2 j