simp only [Var.lc_at] at a1
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
c1 : ¬i < j
c2 : ¬i - j < (List.map free_ zs).length
a1 : Var.lc_at j (bound_ (i - j - (List.map free_ zs).length + j))
⊢ i < j + zs.length
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
c1 : ¬i < j
c2 : ¬i - j < (List.map free_ zs).length
a1 : i - j - (List.map free_ zs).length + j < j
⊢ i < j + zs.length