α✝ : Type u_1
a : α✝
acc : List α✝
n : Nat
⊢ replicate n a ++ a :: acc = replicate n a ++ ([a] ++ acc)
α✝ : Type u_1
a : α✝
acc : List α✝
n : Nat
⊢ replicateTR.loop a (n + 1) acc = replicate (n + 1) a ++ acc
rw [← replicateTR_loop_replicate_eq _ 1 n, replicate, replicate,
replicateTR.loop, replicateTR_loop_eq n, replicateTR_loop_eq n, append_assoc]
no goals
α✝ : Type u_1
a : α✝
acc : List α✝
n : Nat
⊢ replicate n a ++ a :: acc = replicate n a ++ ([a] ++ acc)
rfl