case forall_ x phi phi_ih =>
  unfold Formula.metaVarSet at h1
  unfold sub
  unfold Formula.metaVarSet
  exact phi_ih h1
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : (forall_ x phi).metaVarSet = ∅
⊢ (sub σ τ (forall_ x phi)).metaVarSet = ∅
no goals