rw [get_push, dif_pos h]
case h.h.h.h.h.mk.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
i : Nat
h : i < n
⊢ (push x a)[i] = x[i]
no goals