case nil.def_ X xs =>
  simp only [Holds]
D : Type
I : Interpretation D
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
⊢ Holds D I V M [] (def_ X xs) ↔ Holds D I V M' [] (def_ X xs)
no goals