induction F generalizing vs
F : Formula
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs F
⊢ F.metaVarSet = ∅
case meta_var_
a✝ : MetaVarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ a✝)
⊢ (meta_var_ a✝).metaVarSet = ∅

case pred_
a✝¹ : PredName
a✝ vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ a✝¹ a✝)
⊢ (pred_ a✝¹ a✝).metaVarSet = ∅

case eq_
a✝¹ a✝ : VarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (eq_ a✝¹ a✝)
⊢ (eq_ a✝¹ a✝).metaVarSet = ∅

case true_
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
⊢ true_.metaVarSet = ∅

case not_
a✝ : Formula
a_ih✝ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → a✝.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs a✝.not_
⊢ a✝.not_.metaVarSet = ∅

case imp_
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝¹ → a✝¹.metaVarSet = ∅
a_ih✝ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → a✝.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (a✝¹.imp_ a✝)
⊢ (a✝¹.imp_ a✝).metaVarSet = ∅

case forall_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → a✝.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (forall_ a✝¹ a✝)
⊢ (forall_ a✝¹ a✝).metaVarSet = ∅

case def_
a✝¹ : DefName
a✝ vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ a✝¹ a✝)
⊢ (def_ a✝¹ a✝).metaVarSet = ∅