rewrite [pmap_eq_nat_fold'_push]
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
⊢ size (pmap f as h) = size as
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
⊢ size (Nat.fold' (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) #[]) = size as