rcases A with ⟨h,t⟩
  <;> simp [pop?, back?, getElem?, pop]
α✝ : Type u_1
A' : Array α✝
a : α✝
A : Array α✝
⊢ pop? A = some (A', a) → size A' + 1 = size A
case mk.cons
α✝ : Type u_1
A' : Array α✝
a head✝ : α✝
tail✝ : List α✝
⊢ { data := List.dropLast (head✝ :: tail✝) } = A' →
    { data := head✝ :: tail✝ }[List.length tail✝] = a → size A' = List.length tail✝