specialize a1 v a2
case mp
X : String
vs : List Var
j : ℕ
zs : List String
v : Var
a2 : v ∈ vs
a1 :
  ∀ x ∈ vs,
    Var.openList j (List.map free_ zs) x = Var.openList j (List.map free_ zs) v →
      Var.lc_at j (Var.openList j (List.map free_ zs) v)
⊢ Var.lc_at (j + zs.length) v
case mp
X : String
vs : List Var
j : ℕ
zs : List String
v : Var
a2 : v ∈ vs
a1 :
  Var.openList j (List.map free_ zs) v = Var.openList j (List.map free_ zs) v →
    Var.lc_at j (Var.openList j (List.map free_ zs) v)
⊢ Var.lc_at (j + zs.length) v