induction F generalizing vs
F : Formula
vs : List VarName
v : VarName
Γ : List (VarName × MetaVarName)
h1 : NoMetaVarAndAllFreeInList vs F
h2 : v ∉ vs
⊢ NotFree Γ v F
case meta_var_
v : VarName
Γ : List (VarName × MetaVarName)
a✝ : MetaVarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ a✝)
h2 : v ∉ vs
⊢ NotFree Γ v (meta_var_ a✝)

case pred_
v : VarName
Γ : List (VarName × MetaVarName)
a✝¹ : PredName
a✝ vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ a✝¹ a✝)
h2 : v ∉ vs
⊢ NotFree Γ v (pred_ a✝¹ a✝)

case eq_
v : VarName
Γ : List (VarName × MetaVarName)
a✝¹ a✝ : VarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (eq_ a✝¹ a✝)
h2 : v ∉ vs
⊢ NotFree Γ v (eq_ a✝¹ a✝)

case true_
v : VarName
Γ : List (VarName × MetaVarName)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
h2 : v ∉ vs
⊢ NotFree Γ v true_

case not_
v : VarName
Γ : List (VarName × MetaVarName)
a✝ : Formula
a_ih✝ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → v ∉ vs → NotFree Γ v a✝
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs a✝.not_
h2 : v ∉ vs
⊢ NotFree Γ v a✝.not_

case imp_
v : VarName
Γ : List (VarName × MetaVarName)
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝¹ → v ∉ vs → NotFree Γ v a✝¹
a_ih✝ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → v ∉ vs → NotFree Γ v a✝
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (a✝¹.imp_ a✝)
h2 : v ∉ vs
⊢ NotFree Γ v (a✝¹.imp_ a✝)

case forall_
v : VarName
Γ : List (VarName × MetaVarName)
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → v ∉ vs → NotFree Γ v a✝
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (forall_ a✝¹ a✝)
h2 : v ∉ vs
⊢ NotFree Γ v (forall_ a✝¹ a✝)

case def_
v : VarName
Γ : List (VarName × MetaVarName)
a✝¹ : DefName
a✝ vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ a✝¹ a✝)
h2 : v ∉ vs
⊢ NotFree Γ v (def_ a✝¹ a✝)