case _ c1 =>
  simp at a3_right
  subst a3_right
  exact 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 : bound_ i' = bound_ i
⊢ i < j
no goals