case forall_ x phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h1
  unfold Formula.metaVarSet at h2
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  exact phi_ih h1 h2
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E (forall_ x phi)
h2 : ∀ X ∈ (forall_ x phi).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (forall_ x phi))
no goals