induction E
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (def_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (def_ X xs) ↔ Holds D I V M E (sub σ τ (def_ X xs))
case nil
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv [] (def_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M [] (τ X')) [] (def_ X xs) ↔
    Holds D I V M [] (sub σ τ (def_ X xs))

case cons
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  IsMetaVarOrAllDefInEnv tail✝ (def_ X xs) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M tail✝ (τ X')) tail✝ (def_ X xs) ↔
      Holds D I V M tail✝ (sub σ τ (def_ X xs)))
h1 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (def_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (head✝ :: tail✝) (τ X')) (head✝ :: tail✝) (def_ X xs) ↔
    Holds D I V M (head✝ :: tail✝) (sub σ τ (def_ X xs))