apply elim_eq_forall
case intro
α : Type u_1
v x : α
⊢ elim {x}
        (fun L _hL =>
          match L, _hL with
          | [], _hL => ⋯.elim
          | x_1 :: tail, _hL => x_1)
        ⋯ =
      v ↔
    x = v
case intro.hmotive
α : Type u_1
v x : α
⊢ ∀ {L : List ?intro.α} {hL : ↑L = ?intro.s.val},
    elim ?intro.s ?intro.f ?intro.h = ?intro.f L hL →
      (elim {x}
            (fun L _hL =>
              match L, _hL with
              | [], _hL => ⋯.elim
              | x_1 :: tail, _hL => x_1)
            ⋯ =
          v ↔
        x = v)

case intro.α
α : Type u_1
v x : α
⊢ Type ?u.15504

case intro.β
α : Type u_1
v x : α
⊢ Type ?u.15505

case intro.s
α : Type u_1
v x : α
⊢ Finset ?intro.α

case intro.f
α : Type u_1
v x : α
⊢ (L : List ?intro.α) → ↑L = ?intro.s.val → ?intro.β

case intro.h
α : Type u_1
v x : α
⊢ ∀ (a b : List ?intro.α) (ha : ↑a = ?intro.s.val) (hb : ↑b = ?intro.s.val), ?intro.f a ha = ?intro.f b hb