case moveLeft
x✝¹ x : PGame
IHl✝ : ∀ (i : LeftMoves x), Acc IsOption (moveLeft x i)
IHr✝ : ∀ (j : RightMoves x), Acc IsOption (moveRight x j)
y x✝ : PGame
i : LeftMoves x✝
IHl : ∀ (i : LeftMoves x✝), Acc IsOption (moveLeft x✝ i)
IHr : ∀ (j : RightMoves x✝), Acc IsOption (moveRight x✝ j)
⊢ Acc IsOption (moveLeft x✝ i)

case moveRight
x✝¹ x : PGame
IHl✝ : ∀ (i : LeftMoves x), Acc IsOption (moveLeft x i)
IHr✝ : ∀ (j : RightMoves x), Acc IsOption (moveRight x j)
y x✝ : PGame
j : RightMoves x✝
IHl : ∀ (i : LeftMoves x✝), Acc IsOption (moveLeft x✝ i)
IHr : ∀ (j : RightMoves x✝), Acc IsOption (moveRight x✝ j)
⊢ Acc IsOption (moveRight x✝ j)
x✝ x : PGame
IHl : ∀ (i : LeftMoves x), Acc IsOption (moveLeft x i)
IHr : ∀ (j : RightMoves x), Acc IsOption (moveRight x j)
y : PGame
h : IsOption y x
⊢ Acc IsOption y
induction' h with _ i _ j
no goals
case moveLeft
x✝¹ x : PGame
IHl✝ : ∀ (i : LeftMoves x), Acc IsOption (moveLeft x i)
IHr✝ : ∀ (j : RightMoves x), Acc IsOption (moveRight x j)
y x✝ : PGame
i : LeftMoves x✝
IHl : ∀ (i : LeftMoves x✝), Acc IsOption (moveLeft x✝ i)
IHr : ∀ (j : RightMoves x✝), Acc IsOption (moveRight x✝ j)
⊢ Acc IsOption (moveLeft x✝ i)
exact IHl i
no goals
case moveRight
x✝¹ x : PGame
IHl✝ : ∀ (i : LeftMoves x), Acc IsOption (moveLeft x i)
IHr✝ : ∀ (j : RightMoves x), Acc IsOption (moveRight x j)
y x✝ : PGame
j : RightMoves x✝
IHl : ∀ (i : LeftMoves x✝), Acc IsOption (moveLeft x✝ i)
IHr : ∀ (j : RightMoves x✝), Acc IsOption (moveRight x✝ j)
⊢ Acc IsOption (moveRight x✝ j)
exact IHr j