induction F generalizing vs
F : Formula
vs : List VarName
σ : Instantiation
τ : MetaInstantiation
h1 : NoMetaVarAndAllFreeInList vs F
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ F)
case meta_var_
σ : Instantiation
τ : MetaInstantiation
a✝ : MetaVarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ a✝)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (meta_var_ a✝))

case pred_
σ : Instantiation
τ : MetaInstantiation
a✝¹ : PredName
a✝ vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ a✝¹ a✝)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (pred_ a✝¹ a✝))

case eq_
σ : Instantiation
τ : MetaInstantiation
a✝¹ a✝ : VarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (eq_ a✝¹ a✝)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (eq_ a✝¹ a✝))

case true_
σ : Instantiation
τ : MetaInstantiation
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ true_)

case not_
σ : Instantiation
τ : MetaInstantiation
a✝ : Formula
a_ih✝ :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ a✝)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs a✝.not_
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ a✝.not_)

case imp_
σ : Instantiation
τ : MetaInstantiation
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝¹ → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ a✝¹)
a_ih✝ :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ a✝)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (a✝¹.imp_ a✝)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (a✝¹.imp_ a✝))

case forall_
σ : Instantiation
τ : MetaInstantiation
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ a✝)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (forall_ a✝¹ a✝)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (forall_ a✝¹ a✝))

case def_
σ : Instantiation
τ : MetaInstantiation
a✝¹ : DefName
a✝ vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ a✝¹ a✝)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (def_ a✝¹ a✝))