cases hd
hd : Var
tl : List Var
h1_left : Var.lc_at 0 hd
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
⊢ ∃ xs, hd :: tl = List.map free_ xs
case free_
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
a✝ : String
h1_left : Var.lc_at 0 (free_ a✝)
⊢ ∃ xs, free_ a✝ :: tl = List.map free_ xs

case bound_
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
a✝ : ℕ
h1_left : Var.lc_at 0 (bound_ a✝)
⊢ ∃ xs, bound_ a✝ :: tl = List.map free_ xs