simp only [getElem_eq_data_get]
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < size (push { data := l } a)
⊢ (push { data := l } a)[i] = if h : i < size { data := l } then { data := l }[i] else a
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < size (push { data := l } a)
⊢ List.get (push { data := l } a).data { val := i, isLt := h } =
    if h : i < size { data := l } then List.get l { val := i, isLt := (_ : i < size { data := l }) } else a