simp only [Function.updateITE]
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
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
x : VarName
a✝ : isFreeIn x h1_phi
⊢ Function.updateITE (Function.updateITE V h1_v (V h1_t)) h1_x d x =
    Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t) x
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
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
h1_2 : ¬h1_x = h1_t
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
V : VarAssignment D
d : D
h1_ih :
  Holds D I (Function.updateITE (Function.updateITE V h1_x d) h1_v (Function.updateITE V h1_x d h1_t)) E h1_phi ↔
    Holds D I (Function.updateITE V h1_x d) E h1_phi'
x : VarName
a✝ : 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_v then if h1_t = h1_x then d else V h1_t else if x = h1_x then d else V x