case pred_ X xs =>
  unfold sub
  unfold NoMetaVarAndAllFreeInList
  exact List.map_subset σ.1 h1
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ X xs)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (pred_ X xs))
no goals