case h.h.h.h
α : Type u_2
f : Type u_1
n : α → f → α
l : α
⊢ scanl n l = scanlTR n l
⊢ @scanl = @scanlTR
funext α f n l
no goals
case h.h.h.h
α : Type u_2
f : Type u_1
n : α → f → α
l : α
⊢ scanl n l = scanlTR n l
simp [scanlTR, scanlTR_go_eq]