simp only [Holds]
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
x y : VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ (eq_ x y).metaVarSet, M X V' ↔ M' X V'
⊢ Holds D I V M (head✝ :: tail✝) (eq_ x y) ↔ Holds D I V M' (head✝ :: tail✝) (eq_ x y)
no goals