simp
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
x : String
h1_left : Var.lc_at 0 (free_ x)
⊢ free_ x :: tl = List.map free_ (x :: xs)
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
x : String
h1_left : Var.lc_at 0 (free_ x)
⊢ tl = List.map free_ xs