tauto
case h1
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.args
⊢ ∀ v ∈ xs, V v = V' v
no goals