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

State before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i : xs.Index × ys.Index
⊢ (prod i).val = (i.fst.val, i.snd.val)
Tactic:
rw [prod, val_bind, val_map]
State after:
no goals