simp only [Var.openList]
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
⊢ V (free_ x) = V (Var.close j (free_ z) (Var.openList j [free_ z] (free_ x)))
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
x : String
a1 : free_ x ∈ vs
h2 : Var.lc_at j (free_ x)
⊢ V (free_ x) = V (Var.close j (free_ z) (free_ x))