case not_ phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h1
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  exact phi_ih h1
E : Env
σ : Instantiation
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
h1 : IsMetaVarOrAllDefInEnv E phi.not_
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi.not_)
no goals