simp only [phi_ih]
case h
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
⊢ Holds D I
      (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)
      E
      (sub
        (Function.updateITE σ x
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x))
        c phi) ↔
    Holds D I (Function.updateITE (V ∘ σ) x d) E phi
case h
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
⊢ Holds D I
      (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))
      E phi ↔
    Holds D I (Function.updateITE (V ∘ σ) x d) E phi