simp only [Var.openList]
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
⊢ V (free_ x') = if Var.openList 0 [free_ z] (free_ x') = free_ z then d else V (Var.openList 0 [free_ z] (free_ x'))
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
⊢ V (free_ x') = if free_ x' = free_ z then d else V (free_ x')