Theorem: List.Index.val_unjoin (Extra/Index/Join.lean)

State before:
α : Type u_1
xss : List (List α)
k : xss.join.Index
⊢ k.unjoin.snd.val = k.val
Tactic:
rw [←join_unjoin k, val_join, unjoin_join]
State after:
no goals