∀ (motive : (x x_1 : SetTheory.PGame) → x.Identical x_1 → Prop) (x x_1 : SetTheory.PGame) (x_2 : x.Identical x_1),
  (∀ (α β : Type u_1) (a : α → SetTheory.PGame) (a_1 : β → SetTheory.PGame) (α_1 β_1 : Type u_1)
      (a_2 : α_1 → SetTheory.PGame) (a_3 : β_1 → SetTheory.PGame)
      (hL₁ : Relator.LeftTotal fun i j => (a i).Identical (a_2 j))
      (hL₂ : Relator.RightTotal fun i j => (a i).Identical (a_2 j))
      (hR₁ : Relator.LeftTotal fun i j => (a_1 i).Identical (a_3 j))
      (hR₂ : Relator.RightTotal fun i j => (a_1 i).Identical (a_3 j)),
      motive (SetTheory.PGame.mk α β a a_1) (SetTheory.PGame.mk α_1 β_1 a_2 a_3) ⋯) →
    motive x x_1 x_2