case not_ h1_phi h1_v h1_t h1_phi' _ h1_ih =>
  simp only [Holds]
  congr! 1
  apply h1_ih
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
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 h1_phi.not_ ↔ Holds D I V E h1_phi'.not_
no goals