simp at c1
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : ¬i' < j
a3_right :
  (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)) =
    bound_ i
⊢ i < j
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
a3_right :
  (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)) =
    bound_ i
c1 : j ≤ i'
⊢ i < j