case _ i =>
  simp only [Var.lc_at] at h2
  simp only [Var.openList]
  simp
  split_ifs
  simp only [Var.close]
  simp only [if_pos h2]
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : Var.lc_at j (bound_ i)
⊢ V (bound_ i) = V (Var.close j (free_ z) (Var.openList j [free_ z] (bound_ i)))
no goals