case eq_2_eq_ x_0 x_1 y_0 y_1 =>
  intro D I V E _
  simp only [Holds]
  intro a2
  cases a2
  case _ a2_left a2_right =>
    simp only [a2_left]
    simp only [a2_right]
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E (((eq_ x_0 y_0).and_ (eq_ x_1 y_1)).imp_ ((eq_ x_0 x_1).iff_ (eq_ y_0 y_1)))
no goals