Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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
Tactic:
induction F
Proof state after:
case cons.meta_var_
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✝
a✝ : MetaVarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (meta_var_ a✝)
⊢ IsMetaVarOrAllDefInEnv E' (meta_var_ a✝)

case cons.pred_
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✝
a✝¹ : PredName
a✝ : List VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (pred_ a✝¹ a✝)
⊢ IsMetaVarOrAllDefInEnv E' (pred_ a✝¹ a✝)

case cons.eq_
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✝
a✝¹ a✝ : VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (eq_ a✝¹ a✝)
⊢ IsMetaVarOrAllDefInEnv E' (eq_ a✝¹ a✝)

case cons.true_
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✝
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) true_
⊢ IsMetaVarOrAllDefInEnv E' true_

case cons.not_
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✝
a✝ : Formula
a_ih✝ : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) a✝ → IsMetaVarOrAllDefInEnv E' a✝
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) a✝.not_
⊢ IsMetaVarOrAllDefInEnv E' a✝.not_

case cons.imp_
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✝
a✝¹ a✝ : Formula
a_ih✝¹ : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) a✝¹ → IsMetaVarOrAllDefInEnv E' a✝¹
a_ih✝ : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) a✝ → IsMetaVarOrAllDefInEnv E' a✝
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (a✝¹.imp_ a✝)
⊢ IsMetaVarOrAllDefInEnv E' (a✝¹.imp_ a✝)

case cons.forall_
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✝
a✝¹ : VarName
a✝ : Formula
a_ih✝ : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) a✝ → IsMetaVarOrAllDefInEnv E' a✝
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (forall_ a✝¹ a✝)
⊢ IsMetaVarOrAllDefInEnv E' (forall_ a✝¹ a✝)

case cons.def_
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✝
a✝¹ : DefName
a✝ : List VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (def_ a✝¹ a✝)
⊢ IsMetaVarOrAllDefInEnv E' (def_ a✝¹ a✝)