case meta_var_ X =>
  unfold NoMetaVarAndAllFreeInList at h1
  contradiction
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ X)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (meta_var_ X))
no goals