case cons hd tl ih =>
  simp at h1
  cases h1
  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 : ∀ v ∈ hd :: tl, Var.lc_at 0 v
⊢ ∃ xs, hd :: tl = List.map free_ xs
no goals