unfold sub
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (forall_ x phi))
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (forall_ (↑σ x) (sub σ τ phi))