∀ (motive : (x x_1 : SetTheory.PGame) → x.Short → x_1.Short → Sort u_2) (xl xr : Type u_1) (xL : xl → SetTheory.PGame)
  (xR : xr → SetTheory.PGame) (yl yr : Type u_1) (yL : yl → SetTheory.PGame) (yR : yr → SetTheory.PGame)
  (x : (SetTheory.PGame.mk xl xr xL xR).Short) (x_1 : (SetTheory.PGame.mk yl yr yL yR).Short)
  (h_1 :
    (xl xr : Type u_1) →
      (xL : xl → SetTheory.PGame) →
        (xR : xr → SetTheory.PGame) →
          (yl yr : Type u_1) →
            (yL : yl → SetTheory.PGame) →
              (yR : yr → SetTheory.PGame) →
                (x : (SetTheory.PGame.mk xl xr xL xR).Short) →
                  (x_2 : (SetTheory.PGame.mk yl yr yL yR).Short) →
                    motive (SetTheory.PGame.mk xl xr xL xR) (SetTheory.PGame.mk yl yr yL yR) x x_2),
  (match SetTheory.PGame.mk xl xr xL xR, SetTheory.PGame.mk yl yr yL yR, x, x_1 with
    | SetTheory.PGame.mk xl xr xL xR, SetTheory.PGame.mk yl yr yL yR, x, x_2 => h_1 xl xr xL xR yl yr yL yR x x_2) =
    h_1 xl xr xL xR yl yr yL yR x x_1