unfold NoMetaVarAndAllFreeInList at h1
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
psi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ psi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (phi.imp_ psi)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (phi.imp_ psi))
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
psi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ psi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (phi.imp_ psi))