cases v
case h.h1
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
v : Var
a1 : occursFreeIn v F
⊢ shift D V d v = if Var.openList 0 [free_ z] v = free_ z then d else V (Var.openList 0 [free_ z] v)
case h.h1.free_
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
a✝ : String
a1 : occursFreeIn (free_ a✝) F
⊢ shift D V d (free_ a✝) =
    if Var.openList 0 [free_ z] (free_ a✝) = free_ z then d else V (Var.openList 0 [free_ z] (free_ a✝))

case h.h1.bound_
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
a✝ : ℕ
a1 : occursFreeIn (bound_ a✝) F
⊢ shift D V d (bound_ a✝) =
    if Var.openList 0 [free_ z] (bound_ a✝) = free_ z then d else V (Var.openList 0 [free_ z] (bound_ a✝))