simp only [get_replicate, get_push]
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
⊢ (replicate (n + 1) a)[i] = (push (replicate n a) a)[i]
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
⊢ a = if h : i < n then a else a