case
  forall_free_in h1_x h1_phi h1_v h1_t h1_phi' h1_1 h1_2 _ h1_ih
| exists_free_in h1_x h1_phi h1_v h1_t h1_phi' h1_1 h1_2 _ h1_ih =>
  simp only [isFreeIn] at h1_1
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  specialize h1_ih (Function.updateITE V h1_x d)
  simp only [← h1_ih]
  apply Holds_coincide_Var
  intro x _
  simp only [Function.updateITE]
  simp only [eq_comm]
  split_ifs
  case _ c1 c2 c3 =>
    subst c2
    cases h1_1
    case intro h1_1_left h1_1_right =>
      contradiction
  case _ | _ | _ =>
    rfl
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 : isFreeIn h1_v (exists_ h1_x h1_phi)
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi')
no goals