cases hL
case intro.hmotive
α : Type u_1
v x : α
L : List α
hL✝ : ↑L = {x}.val
hL : L = [x]
⊢ (match L, hL✝ with
      | [], _hL => ⋯.elim
      | x_1 :: tail, _hL => x_1) =
      v ↔
    x = v
case intro.hmotive.refl
α : Type u_1
v x : α
hL : ↑[x] = {x}.val
⊢ (match [x], hL with
      | [], _hL => ⋯.elim
      | x_1 :: tail, _hL => x_1) =
      v ↔
    x = v