case eq_ x y =>
  unfold IsMetaVarOrAllDefInEnv
  simp only
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 y : VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (eq_ x y)
⊢ IsMetaVarOrAllDefInEnv E' (eq_ x y)
no goals