cases h1
hd : Var
tl : List Var
ih : (∀ v ∈ tl, Var.lc_at 0 v) → ∃ xs, tl = List.map free_ xs
h1 : Var.lc_at 0 hd ∧ ∀ a ∈ tl, Var.lc_at 0 a
⊢ ∃ xs, hd :: tl = List.map free_ xs
case intro
hd : Var
tl : List Var
ih : (∀ v ∈ tl, Var.lc_at 0 v) → ∃ xs, tl = List.map free_ xs
left✝ : Var.lc_at 0 hd
right✝ : ∀ a ∈ tl, Var.lc_at 0 a
⊢ ∃ xs, hd :: tl = List.map free_ xs