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