induction E
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
⊢ IsNotFree D I M E (def_ X xs) v
case nil
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M [] (meta_var_ X) v
⊢ IsNotFree D I M [] (def_ X xs) v

case cons
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M tail✝ (meta_var_ X) v) → IsNotFree D I M tail✝ (def_ X xs) v
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M (head✝ :: tail✝) (meta_var_ X) v
⊢ IsNotFree D I M (head✝ :: tail✝) (def_ X xs) v