show (cons a x).val[0]'((cons a x).size_eq.symm ▸ hi) = a
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
hi : 0 < n + 1
⊢ (cons a x)[0] = a
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
hi : 0 < n + 1
⊢ (cons a x).val[0] = a