(motive : (x : List SetTheory.PGame) → SetTheory.PGame.ListShort x → (x_2 : ℕ) → x_2 < x.length → Sort u_2) →
  (x : List SetTheory.PGame) →
    (x_1 : SetTheory.PGame.ListShort x) →
      (x_2 : ℕ) →
        (x_3 : x_2 < x.length) →
          ((head : SetTheory.PGame) →
              (tail : List SetTheory.PGame) →
                (S : head.Short) →
                  (a : SetTheory.PGame.ListShort tail) →
                    (x : 0 < (head :: tail).length) → motive (head :: tail) (SetTheory.PGame.ListShort.cons' S a) 0 x) →
            ((head : SetTheory.PGame) →
                (tl : List SetTheory.PGame) →
                  (a : head.Short) →
                    (S : SetTheory.PGame.ListShort tl) →
                      (n : ℕ) →
                        (h : n + 1 < (head :: tl).length) →
                          motive (head :: tl) (SetTheory.PGame.ListShort.cons' a S) n.succ h) →
              motive x x_1 x_2 x_3