split at a1
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
a1 :
  Var.lc_at j
    (if i < j then bound_ i
    else
      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
case inl
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
h✝ : i < j
a1 : Var.lc_at j (bound_ i)
⊢ i < j + zs.length

case inr
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
h✝ : ¬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