dsimp [cons]
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 < n + 1
hi₂ : i < n
⊢ List.get (cons a x).val.data { val := i + 1, isLt := (_ : i + 1 < Array.size (cons a x).val) } =
    List.get x.val.data { val := i, isLt := (_ : i < Array.size x.val) }
no goals