∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {as bs : Array α},
  as = bs → ∀ {f g : α → m (Option β)}, (∀ (a : α), f a = g a) → Array.filterMapM f as = Array.filterMapM g bs