simp only [List.concat_eq_append]
α : 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₂
α : Type u
β : Type v
n : Nat
a₁ a₂ : α
x : SizedArray α n
⊢ a₁ :: x.val.data ++ [a₂] = a₁ :: (x.val.data ++ [a₂])