Theorem: Subarray.getElem_shrinkOne' (Algdata/Data/Array/Subarray.lean)

State before:
α : Type u
x : Subarray α
h : x.start < x.stop
i : Nat
hi : i < size (shrinkOne' x h)
⊢ (shrinkOne' x h)[i] = x[i]
Tactic:
rfl
State after:
no goals