split_ifs
case h.h1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
⊢ Function.updateITE V
      (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet else x) d
      (Function.updateITE σ x
        (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet else x)
        v) =
    Function.updateITE (V ∘ σ) x d v
case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
h✝ : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
⊢ Function.updateITE V (fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet) d
      (Function.updateITE σ x (fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet) v) =
    Function.updateITE (V ∘ σ) x d v

case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
h✝ : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
⊢ Function.updateITE V x d (Function.updateITE σ x x v) = Function.updateITE (V ∘ σ) x d v