case h.h.h.h
α : Type u_1
f : α → α
n : Nat
l : List α
⊢ modifyNth f n l = modifyNthTR f n l
⊢ @modifyNth = @modifyNthTR
funext α f n l
no goals
case h.h.h.h
α : Type u_1
f : α → α
n : Nat
l : List α
⊢ modifyNth f n l = modifyNthTR f n l
simp [modifyNthTR, modifyNthTR_go_eq]