simp only [Holds]
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_psi h1_psi' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_psi h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ Holds D I V E (h1_phi.iff_ h1_psi) ↔ Holds D I V E (h1_phi'.iff_ h1_psi')
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_psi h1_psi' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_psi h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ (Holds D I V E h1_phi ↔ Holds D I V E h1_psi) ↔ (Holds D I V E h1_phi' ↔ Holds D I V E h1_psi')