Theorem: List.Index.val_unoption (Extra/Index/Option.lean)

State before:
α : Type u_1
xs : List α
k : xs.option.Index
⊢ k.val =
    match k.unoption with
    | none => none
    | some k => some k.val
Tactic:
rw [←option_unoption k, val_option, unoption_option]
State after:
no goals