conv =>
  lhs; arg 2
  change f ((push x a)[n]'n.lt_succ_self) b
  rw [get_push, dif_neg n.lt_irrefl]
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ push (mapIdx (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) y)
      (f (push x a)[{ val := n, isLt := (_ : n < Nat.succ n) }] b) =
    push (mapIdx (fun i => f x[i]) y) (f a b)
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ push (mapIdx (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) y) (f a b) =
    push (mapIdx (fun i => f x[i]) y) (f a b)