Theorem: List.Index.arr_unarr (Extra/Index/Arr.lean)

State before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
k : (xs.arr ys).Index
⊢ arr k.unarr = k
Tactic:
rw [arr, unarr, pi_unpi]
State after:
no goals