case pred_ X xs =>
  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 : PredName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (pred_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
⊢ Holds D I V M (head✝ :: tail✝) (pred_ X xs) ↔ Holds D I V M' (head✝ :: tail✝) (pred_ X xs)
no goals