case h.h.h.h
α : Type u_1
n : Nat
a : α
l : List α
⊢ leftpad n a l = leftpadTR n a l
⊢ @leftpad = @leftpadTR
funext α n a l
no goals
case h.h.h.h
α : Type u_1
n : Nat
a : α
l : List α
⊢ leftpad n a l = leftpadTR n a l
simp [leftpad, leftpadTR, replicateTR_loop_eq]