simp only [Var.lc_at]
X : String
vs : List Var
j : ℕ
zs : List String
x : String
a2 : free_ x ∈ vs
a1 : Var.lc_at j (Var.openList j (List.map free_ zs) (free_ x))
⊢ Var.lc_at (j + zs.length) (free_ x)
no goals