case forall_ x phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h2
  unfold IsMetaVarOrAllDefInEnv
  exact phi_ih h2
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (forall_ x phi)
⊢ IsMetaVarOrAllDefInEnv E' (forall_ x phi)
no goals