Theorem: List.Index.val_unbind (Extra/Index/Bind.lean)

State before:
α : Type u_1
β : Type u_2
f : α → List β
xs : List α
i : (xs.bind f).Index
⊢ (unbind f i).snd.val = i.val
Tactic:
rw [←bind_unbind f i, val_bind, unbind_bind]
State after:
no goals