unfold Formula.metaVarSet at h1
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : (meta_var_ X).metaVarSet = ∅
⊢ (sub σ τ (meta_var_ X)).metaVarSet = ∅
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : {X} = ∅
⊢ (sub σ τ (meta_var_ X)).metaVarSet = ∅