case def_iff_ phi psi =>
  intro D I V E _
  simp only [Holds]
  tauto
Δ : List Formula
F phi psi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E
        (((phi.iff_ psi).imp_ ((phi.imp_ psi).imp_ (psi.imp_ phi).not_).not_).imp_
            (((phi.imp_ psi).imp_ (psi.imp_ phi).not_).not_.imp_ (phi.iff_ psi)).not_).not_
no goals