simp only [Function.updateITE]
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 = Function.updateITE V (free_ z) d (Var.openList 0 [free_ z] 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)