unfold sub
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ X xs)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (def_ X xs))
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ X xs)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (def_ X (List.map (↑σ) xs))