case _ i =>
  simp only [Var.lc_at]
  simp only [Var.openList] at a1
  split at a1
  case _ c1 =>
    linarith
  case _ c1 =>
    split at a1
    case _ c2 =>
      simp at c2
      exact lt_add_of_tsub_lt_left c2
    case _ c2 =>
      simp only [Var.lc_at] at a1
      simp at a1
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
a1 : Var.lc_at j (Var.openList j (List.map free_ zs) (bound_ i))
⊢ Var.lc_at (j + zs.length) (bound_ i)
no goals