rfl
α : Type u
β : Type v
γ : Type w
n : Nat
f : α → β
g : β → γ
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map (g ∘ f) x = map g (map f x)
⊢ push (map g (map f x)) ((g ∘ f) a) = push (map g (map f x)) (g (f a))
no goals