induction E generalizing F
E E' : Env
F : Formula
h1 : ∃ E1, E' = E1 ++ E
h2 : IsMetaVarOrAllDefInEnv E F
⊢ IsMetaVarOrAllDefInEnv E' F
case nil
E' : Env
F : Formula
h1 : ∃ E1, E' = E1 ++ []
h2 : IsMetaVarOrAllDefInEnv [] F
⊢ IsMetaVarOrAllDefInEnv E' F

case cons
E' : Env
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : ∀ (F : Formula), (∃ E1, E' = E1 ++ tail✝) → IsMetaVarOrAllDefInEnv tail✝ F → IsMetaVarOrAllDefInEnv E' F
F : Formula
h1 : ∃ E1, E' = E1 ++ head✝ :: tail✝
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) F
⊢ IsMetaVarOrAllDefInEnv E' F