case _ c1 =>
  split at a1
  case _ c2 =>
    simp at c2
    exact lt_add_of_tsub_lt_left c2
  case _ c2 =>
    simp only [Var.lc_at] at a1
    simp at a1
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
c1 : ¬i < j
a1 :
  Var.lc_at j
    (if x : i - j < (List.map free_ zs).length then (List.map free_ zs)[i - j]
    else bound_ (i - j - (List.map free_ zs).length + j))
⊢ i < j + zs.length
no goals