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