induction E generalizing F vs V V'
D : Type
I : Interpretation D
V V' : Valuation D
M : MetaValuation D
E : Env
F : Formula
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs F
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M E F ↔ Holds D I V' M E F
case nil
D : Type
I : Interpretation D
M : MetaValuation D
V V' : Valuation D
F : Formula
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs F
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M [] F ↔ Holds D I V' M [] F

case cons
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
V V' : Valuation D
F : Formula
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs F
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) F ↔ Holds D I V' M (head✝ :: tail✝) F