∀ {motive : SetTheory.PGame → Sort u_1} (t : SetTheory.PGame)
  (F_1 : (t : SetTheory.PGame) → SetTheory.PGame.below t → motive t),
  SetTheory.PGame.brecOn t F_1 = F_1 t (SetTheory.PGame.brecOn.go t F_1).2