unfold sub
σ : Instantiation
τ : MetaInstantiation
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ true_)
σ : Instantiation
τ : MetaInstantiation
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) true_