specialize h1 v a1
case h1
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
v : Var
a1 : v ∈ vs
⊢ Var.openList j (List.map free_ zs) v = v
case h1
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
h1 : Var.lc_at j v
⊢ Var.openList j (List.map free_ zs) v = v