Theorem: List.Index.val_unprod (Extra/Index/Prod.lean)

State before:
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
⊢ (i.unprod.fst.val, i.unprod.snd.val) = i.val
Tactic:
rw [←prod_unprod i, val_prod, unprod_prod]
State after:
no goals