induction F
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F : Formula
Γ : List (VarName × MetaVarName)
v : VarName
h1 : NotFree Γ v F
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
⊢ IsNotFree D I M E F v
case meta_var_
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
a✝ : MetaVarName
h1 : NotFree Γ v (meta_var_ a✝)
⊢ IsNotFree D I M E (meta_var_ a✝) v

case pred_
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
a✝¹ : PredName
a✝ : List VarName
h1 : NotFree Γ v (pred_ a✝¹ a✝)
⊢ IsNotFree D I M E (pred_ a✝¹ a✝) v

case eq_
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
a✝¹ a✝ : VarName
h1 : NotFree Γ v (eq_ a✝¹ a✝)
⊢ IsNotFree D I M E (eq_ a✝¹ a✝) v

case true_
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
h1 : NotFree Γ v true_
⊢ IsNotFree D I M E true_ v

case not_
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
a✝ : Formula
a_ih✝ : NotFree Γ v a✝ → IsNotFree D I M E a✝ v
h1 : NotFree Γ v a✝.not_
⊢ IsNotFree D I M E a✝.not_ v

case imp_
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
a✝¹ a✝ : Formula
a_ih✝¹ : NotFree Γ v a✝¹ → IsNotFree D I M E a✝¹ v
a_ih✝ : NotFree Γ v a✝ → IsNotFree D I M E a✝ v
h1 : NotFree Γ v (a✝¹.imp_ a✝)
⊢ IsNotFree D I M E (a✝¹.imp_ a✝) v

case forall_
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
a✝¹ : VarName
a✝ : Formula
a_ih✝ : NotFree Γ v a✝ → IsNotFree D I M E a✝ v
h1 : NotFree Γ v (forall_ a✝¹ a✝)
⊢ IsNotFree D I M E (forall_ a✝¹ a✝) v

case def_
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
a✝¹ : DefName
a✝ : List VarName
h1 : NotFree Γ v (def_ a✝¹ a✝)
⊢ IsNotFree D I M E (def_ a✝¹ a✝) v