apply E_ih
case neg
D : Type
I : Interpretation D
E_hd : Definition
E_tl : List Definition
E_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 E_tl F ↔ Holds D I V M' E_tl F)
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'
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I V M E_tl (def_ X xs) ↔ Holds D I V M' E_tl (def_ X xs)
case neg.h1
D : Type
I : Interpretation D
E_hd : Definition
E_tl : List Definition
E_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 E_tl F ↔ Holds D I V M' E_tl F)
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'
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'