dsimp [back, Array.back']
α : Type u
β : Type v
n : Nat
x : SizedArray α (n + 1)
⊢ back x = Array.back' x.val (_ : Array.size x.val > 0)
α : Type u
β : Type v
n : Nat
x : SizedArray α (n + 1)
⊢ x[n] = x.val[Array.size x.val - 1]