intro i hi x hx
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
⊢ ∀ (i : Nat) (hi : i < size as) (a : Array β),
    (fun k x => size x = k) i a →
      (fun k x => size x = k) (i + 1)
        (push a (f as[{ val := i, isLt := hi }.val] (_ : p as[{ val := i, isLt := hi }.val])))
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size as
x : Array β
hx : size x = i
⊢ size (push x (f as[{ val := i, isLt := hi }.val] (_ : p as[{ val := i, isLt := hi }.val]))) = i + 1