Theorem: List.Index.val_unappend (Extra/Index/Append.lean)

State before:
α : Type u_1
xs ys : List α
k : (xs ++ ys).Index
⊢ (match k.unappend with
    | Sum.inl i => i.val
    | Sum.inr j => j.val) =
    k.val
Tactic:
rw [←append_unappend k, val_append, unappend_append]
State after:
no goals