Theorem: Vec.getElem_eq_getElem (QuickSortInLean/Vec.lean)

State before:
α : Type
n : Nat
a : Vec α n
i : Fin n
⊢ a[i] = a.val[↑i]
Tactic:
rfl
State after:
no goals