case _ x =>
  simp only [Var.openList] at a3_right
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
x : String
a3_left : free_ x ∈ vs
a3_right : Var.openList j (List.map free_ zs) (free_ x) = bound_ i
a1 : Var.lc_at (j + zs.length) (free_ x)
⊢ i < j
no goals