specialize h2 v a1
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
v : Var
a1 : v ∈ vs
⊢ V v = ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) v
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
v : Var
a1 : v ∈ vs
h2 : Var.lc_at j v
⊢ V v = ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) v