congr! 1
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ ¬Holds D I V E h1_phi ↔ ¬Holds D I V E h1_phi'
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi'