case _ i =>
  simp only [Var.lc_at]
  simp at a2
  apply Exists.elim a2
  intro z a3
  clear a2
  cases a3
  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 : ℕ
a2 : bound_ i ∈ List.map (Var.openList j (List.map free_ zs)) vs
⊢ Var.lc_at j (bound_ i)
no goals