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