dsimp [push,cons, Array.push]
α : Type u
β : Type v
n : Nat
a₁ a₂ : α
x : SizedArray α n
⊢ (push (cons a₁ x) a₂).val.data = (cons a₁ (push x a₂)).val.data
α : Type u
β : Type v
n : Nat
a₁ a₂ : α
x : SizedArray α n
⊢ List.concat (a₁ :: x.val.data) a₂ = a₁ :: List.concat x.val.data a₂