case symm_ h1_phi h1_phi' _ h1_ih =>
  symm
  exact h1_ih V
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
no goals