simp
case h.succ
α : Type u_1
a : α
n : Nat
ih : a :: List.replicate n a = List.replicate n a ++ [a]
⊢ a :: List.replicate (Nat.succ n) a = List.replicate (Nat.succ n) a ++ [a]
case h.succ
α : Type u_1
a : α
n : Nat
ih : a :: List.replicate n a = List.replicate n a ++ [a]
⊢ a :: List.replicate n a = List.replicate n a ++ [a]