English
If x and y have equivalent left/moves and right/moves under an equivalence between their moves, then x ≡ y.
Русский
Если между лeвыми и правыми ходами x и y существует эквивалентность, переводящая x в y, то x ≡ y.
LaTeX
$$$ \forall {x y : PGame} (l : x.LeftMoves \simeq y.LeftMoves) (r : x.RightMoves \simeq y.RightMoves) \\ (hl : \forall i, x.moveLeft i \equiv y.moveLeft (l i)) (hr : \forall i, x.moveRight i \equiv y.moveRight (r i)) : x \equiv y$$$
Lean4
theorem of_equiv {x y : PGame} (l : x.LeftMoves ≃ y.LeftMoves) (r : x.RightMoves ≃ y.RightMoves)
(hl : ∀ i, x.moveLeft i ≡ y.moveLeft (l i)) (hr : ∀ i, x.moveRight i ≡ y.moveRight (r i)) : x ≡ y :=
.of_fn l l.symm r r.symm hl (by simpa using hl <| l.symm ·) hr (by simpa using hr <| r.symm ·)
