simp only [map_data', cons]
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
a : α
x : Array α
⊢ (map f (cons a x)).data = (cons (f a) (map f x)).data
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
a : α
x : Array α
⊢ List.map f (a :: x.data) = f a :: List.map f x.data