Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
i : ℤ
⊢ nth (move Dir.right T) i = nth (move Dir.left (move Dir.right T)) (i + 1)
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
i : ℤ
⊢ nth (move Dir.right T) i = nth T (i + 1)
conv => rhs; rw [← T.move_right_left]
no goals
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
i : ℤ
⊢ nth (move Dir.right T) i = nth (move Dir.left (move Dir.right T)) (i + 1)
rw [Tape.move_left_nth, add_sub_cancel]