rw [map_pure]
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x : Array α
⊢ Subtype.val <$> pure { val := #[], property := (_ : size #[] = size #[]) } = mapM f #[]
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x : Array α
⊢ pure { val := #[], property := (_ : size #[] = size #[]) }.val = mapM f #[]