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
i i' : ℕ
a3_left : bound_ i' ∈ vs
a3_right : Var.openList j (List.map free_ zs) (bound_ i') = bound_ i
a1 : Var.lc_at (j + zs.length) (bound_ i')
⊢ i < j
no goals