split_ifs
case h.h1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
⊢ (if x = h1_x then d else if x = h1_v then V h1_t else V x) = if x = h1_x then d else V x
case pos
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
h✝ : x = h1_x
⊢ d = d

case pos
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
h✝¹ : ¬x = h1_x
h✝ : x = h1_v
⊢ V h1_t = V x

case neg
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
V : VarAssignment D
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
d : D
x : VarName
a1 : isFreeIn x h1_phi
h✝¹ : ¬x = h1_x
h✝ : ¬x = h1_v
⊢ V x = V x