unfold NotFree at h1
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
h1 : NotFree Γ v (def_ X xs)
E_hd : Definition
E_tl : List Definition
E_ih : (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E_tl (meta_var_ X) v) → IsNotFree D I M E_tl (def_ X xs) v
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M (E_hd :: E_tl) (meta_var_ X) v
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v
D : Type
I : Interpretation D
M : MetaValuation D
Γ : List (VarName × MetaVarName)
v : VarName
X : DefName
xs : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : (∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E_tl (meta_var_ X) v) → IsNotFree D I M E_tl (def_ X xs) v
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M (E_hd :: E_tl) (meta_var_ X) v
h1 : v ∉ xs
⊢ IsNotFree D I M (E_hd :: E_tl) (def_ X xs) v