apply forall_congr'
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ (∀ (d : D), Holds D I (Function.updateITE V h1_x d) E h1_phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V h1_x d) E h1_psi
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ ∀ (a : D), Holds D I (Function.updateITE V h1_x a) E h1_phi ↔ Holds D I (Function.updateITE V h1_x a) E h1_psi