cases 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))
case a.h.e'_4.free_
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
a✝ : String
a1 : free_ a✝ ∈ vs
h2 : Var.lc_at j (free_ a✝)
⊢ V (free_ a✝) = V (Var.close j (free_ z) (Var.openList j [free_ z] (free_ a✝)))

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