cases h2_1
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
h2_1 : d ∈ E_hd :: E_tl ∧ X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
case intro
E' : Env
E_hd : Definition
E_tl : List Definition
E_ih : ∀ (F : Formula), (∃ E1, E' = E1 ++ E_tl) → IsMetaVarOrAllDefInEnv E_tl F → IsMetaVarOrAllDefInEnv E' F
h1 : ∃ E1, E' = E1 ++ E_hd :: E_tl
X : DefName
xs : List VarName
h2 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E_hd :: E_tl
d : Definition
left✝ : d ∈ E_hd :: E_tl
right✝ : X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)