specialize ih h1_right
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
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, hd :: tl = List.map free_ xs