case intro h1_left h1_right =>
  specialize ih h1_right
  apply Exists.elim ih
  intro xs a1
  cases hd
  case free_ x =>
    apply Exists.intro (x :: xs)
    simp
    exact a1
  case bound_ i =>
    simp only [Var.lc_at] at h1_left
    simp at h1_left
hd : Var
tl : List Var
ih : (∀ v ∈ tl, Var.lc_at 0 v) → ∃ xs, tl = List.map free_ xs
h1_left : Var.lc_at 0 hd
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
⊢ ∃ xs, hd :: tl = List.map free_ xs
no goals