∀ {x y : SetTheory.PGame} (k : (x * y).RightMoves) {P : (x * y).RightMoves → Prop},
  (∀ (ix : x.LeftMoves) (jy : y.RightMoves), P (SetTheory.PGame.toRightMovesMul (Sum.inl (ix, jy)))) →
    (∀ (jx : x.RightMoves) (iy : y.LeftMoves), P (SetTheory.PGame.toRightMovesMul (Sum.inr (jx, iy)))) → P k