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

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