unfold IsMetaVarOrAllDefInEnv at h1
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (forall_ (↑σ x) (sub σ τ phi))
⊢ IsMetaVarOrAllDefInEnv E (forall_ x phi)
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
⊢ IsMetaVarOrAllDefInEnv E (forall_ x phi)