case meta_var_ X =>
  unfold Formula.metaVarSet at h1
  simp at h1
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : (meta_var_ X).metaVarSet = ∅
⊢ (sub σ τ (meta_var_ X)).metaVarSet = ∅
no goals