{J : CategoryTheory.Limits.MultispanShape} →
  {motive : (x x_1 : CategoryTheory.Limits.WalkingMultispan J) → x.Hom x_1 → Sort u} →
    {x x_1 : CategoryTheory.Limits.WalkingMultispan J} →
      (t : x.Hom x_1) →
        ((A : CategoryTheory.Limits.WalkingMultispan J) →
            motive A A (CategoryTheory.Limits.WalkingMultispan.Hom.id A)) →
          ((a : J.L) →
              motive (CategoryTheory.Limits.WalkingMultispan.left a)
                (CategoryTheory.Limits.WalkingMultispan.right (J.fst a))
                (CategoryTheory.Limits.WalkingMultispan.Hom.fst a)) →
            ((a : J.L) →
                motive (CategoryTheory.Limits.WalkingMultispan.left a)
                  (CategoryTheory.Limits.WalkingMultispan.right (J.snd a))
                  (CategoryTheory.Limits.WalkingMultispan.Hom.snd a)) →
              motive x x_1 t