case not_ phi phi_ih =>
  unfold NoMetaVarAndAllFreeInList at h1
  unfold sub
  unfold NoMetaVarAndAllFreeInList
  exact phi_ih vs h1
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi.not_
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi.not_)
no goals