simp only [Array.getElem_eq_data_get]
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
hi : 0 < n + 1
⊢ (cons a x).val[0] = a
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
hi : 0 < n + 1
⊢ List.get (cons a x).val.data { val := 0, isLt := (_ : 0 < Array.size (cons a x).val) } = a