case bound_ i =>
  simp only [Var.lc_at] at h1_left
  simp at h1_left
tl : List Var
h1_right : ∀ a ∈ tl, Var.lc_at 0 a
ih : ∃ xs, tl = List.map free_ xs
xs : List String
a1 : tl = List.map free_ xs
i : ℕ
h1_left : Var.lc_at 0 (bound_ i)
⊢ ∃ xs, bound_ i :: tl = List.map free_ xs
no goals