{ι : Type u_1} →
  [inst : LinearOrder ι] →
    (motive :
        CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι) → Sort u_2) →
      (i : CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι)) →
        ((a : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).L) →
            motive (CategoryTheory.Limits.WalkingMultispan.left a)) →
          ((a : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).R) →
              motive (CategoryTheory.Limits.WalkingMultispan.right a)) →
            motive i