English
A right move of x corresponds to a relabelling of a right move of y under a relabelling between x and y. Precisely, for any r: x ≡r y and i in x.RightMoves, x.moveRight i ≡r y.moveRight (r.rightMovesEquiv i).
Русский
Правый ход x соответствует через релятабелирование правому ходу y; для любого r: x ≡r y и любого i ∈ x.RightMoves, x.moveRight i эквивалентно через релятабелирование y.moveRight (r.rightMovesEquiv i).
LaTeX
$$$ \\forall r : x \\equiv_r y, \\forall i : x.RightMoves,\\ x.moveRight i \\equiv_r y.moveRight (r.rightMovesEquiv i). $$$
Lean4
/-- A right move of `x` is a relabelling of a right move of `y`. -/
def moveRight : ∀ (r : x ≡r y) (i : x.RightMoves), x.moveRight i ≡r y.moveRight (r.rightMovesEquiv i)
| ⟨_, _, _, hR⟩ => hR
