case _ a3_left a3_right =>
  specialize a1 z a3_left
  cases z
  case _ x =>
    simp only [Var.openList] at a3_right
  case _ i' =>
    simp only [Var.lc_at] at a1
    simp only [Var.openList] at a3_right
    split at a3_right
    case _ c1 =>
      simp at a3_right
      subst a3_right
      exact c1
    case _ c1 =>
      simp at c1
      simp at a3_right
      split at a3_right
      case _ c2 =>
        contradiction
      case _ c2 =>
        exfalso
        apply c2
        exact Nat.sub_lt_left_of_lt_add c1 a1
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
i : ℕ
z : Var
a3_left : z ∈ vs
a3_right : Var.openList j (List.map free_ zs) z = bound_ i
⊢ i < j
no goals