English
If r is a relabelling between x and y, then for any i in y.RightMoves, x.moveRight (r.rightMovesEquiv.symm i) is Relabelling-equivalent to y.moveRight i. This captures right-move symmetry under relabelling.
Русский
Если r — релятабелирование между x и y, то для любого i из y.RightMoves, x.moveRight (r.rightMovesEquiv.symm i) эквивалентно через релятабелирование y.moveRight i.
LaTeX
$$$ \\forall r : x \\equiv_r y, \\forall i : y.RightMoves,\\ x.moveRight (r.rightMovesEquiv.symm i) \\equiv_r y.moveRight i. $$$
Lean4
/-- A right move of `y` is a relabelling of a right move of `x`. -/
def moveRightSymm : ∀ (r : x ≡r y) (i : y.RightMoves), x.moveRight (r.rightMovesEquiv.symm i) ≡r y.moveRight i
| ⟨L, R, hL, hR⟩, i => by simpa using hR (R.symm i)
