case _ c2 =>
  simp at c2
  exact lt_add_of_tsub_lt_left c2
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 (List.map free_ zs)[i - j]
⊢ i < j + zs.length
no goals