internlm/Lean-Github huggingface dataset:
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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✝
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
psi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi → IsMetaVarOrAllDefInEnv E' psi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (phi.imp_ psi)
⊢ IsMetaVarOrAllDefInEnv E' (phi.imp_ psi)
Tactic:
unfold IsMetaVarOrAllDefInEnv at h2
Proof state after:
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✝
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
psi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi → IsMetaVarOrAllDefInEnv E' psi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi ∧ IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi
⊢ IsMetaVarOrAllDefInEnv E' (phi.imp_ psi)
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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✝
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
psi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi → IsMetaVarOrAllDefInEnv E' psi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi ∧ IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi
⊢ IsMetaVarOrAllDefInEnv E' (phi.imp_ psi)
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
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✝
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
psi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi → IsMetaVarOrAllDefInEnv E' psi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi ∧ IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi
⊢ IsMetaVarOrAllDefInEnv E' phi ∧ IsMetaVarOrAllDefInEnv E' psi
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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✝
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
psi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi → IsMetaVarOrAllDefInEnv E' psi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi ∧ IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi
⊢ IsMetaVarOrAllDefInEnv E' phi ∧ IsMetaVarOrAllDefInEnv E' psi
Tactic:
cases h2
Proof state after:
case intro
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✝
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
psi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi → IsMetaVarOrAllDefInEnv E' psi
left✝ : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi
right✝ : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi
⊢ IsMetaVarOrAllDefInEnv E' phi ∧ IsMetaVarOrAllDefInEnv E' psi
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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✝
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
psi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi → IsMetaVarOrAllDefInEnv E' psi
h2_left : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi
h2_right : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi
⊢ IsMetaVarOrAllDefInEnv E' phi ∧ IsMetaVarOrAllDefInEnv E' psi
Tactic:
constructor
Proof state after:
case left
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✝
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
psi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi → IsMetaVarOrAllDefInEnv E' psi
h2_left : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi
h2_right : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi
⊢ IsMetaVarOrAllDefInEnv E' phi

case right
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✝
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
psi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi → IsMetaVarOrAllDefInEnv E' psi
h2_left : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi
h2_right : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi
⊢ IsMetaVarOrAllDefInEnv E' psi
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
case left
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✝
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
psi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi → IsMetaVarOrAllDefInEnv E' psi
h2_left : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi
h2_right : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi
⊢ IsMetaVarOrAllDefInEnv E' phi
Tactic:
exact phi_ih h2_left
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
case right
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✝
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
psi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi → IsMetaVarOrAllDefInEnv E' psi
h2_left : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi
h2_right : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) psi
⊢ IsMetaVarOrAllDefInEnv E' psi
Tactic:
exact psi_ih h2_right
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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)
Tactic:
unfold IsMetaVarOrAllDefInEnv at h2
Proof state after:
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✝) phi
⊢ IsMetaVarOrAllDefInEnv E' (forall_ x phi)
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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✝) phi
⊢ IsMetaVarOrAllDefInEnv E' (forall_ x phi)
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
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✝) phi
⊢ IsMetaVarOrAllDefInEnv E' phi
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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✝) phi
⊢ IsMetaVarOrAllDefInEnv E' phi
Tactic:
exact phi_ih h2
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
h1 : ∃ E1, E' = E1 ++ []
X : DefName
xs : List VarName
h2 : IsMetaVarOrAllDefInEnv [] (def_ X xs)
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
Tactic:
unfold IsMetaVarOrAllDefInEnv at h2
Proof state after:
E' : Env
h1 : ∃ E1, E' = E1 ++ []
X : DefName
xs : List VarName
h2 : ∃ d ∈ [], X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E' : Env
h1 : ∃ E1, E' = E1 ++ []
X : DefName
xs : List VarName
h2 : ∃ d ∈ [], X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
Tactic:
simp at h2
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
Tactic:
unfold IsMetaVarOrAllDefInEnv at h2
Proof state after:
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
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
Tactic:
apply Exists.elim h1
Proof state after:
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
⊢ ∀ (a : Env), E' = a ++ E_hd :: E_tl → IsMetaVarOrAllDefInEnv E' (def_ X xs)
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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
⊢ ∀ (a : Env), E' = a ++ E_hd :: E_tl → IsMetaVarOrAllDefInEnv E' (def_ X xs)
Tactic:
intro E1 h1_1
Proof state after:
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
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
Tactic:
apply Exists.elim h2
Proof state after:
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
⊢ ∀ (a : Definition), a ∈ E_hd :: E_tl ∧ X = a.name ∧ xs.length = a.args.length → IsMetaVarOrAllDefInEnv E' (def_ X xs)
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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
⊢ ∀ (a : Definition), a ∈ E_hd :: E_tl ∧ X = a.name ∧ xs.length = a.args.length → IsMetaVarOrAllDefInEnv E' (def_ X xs)
Tactic:
intro d h2_1
Proof state after:
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)
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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)
Tactic:
cases h2_1
Proof state after:
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)
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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_left : d ∈ E_hd :: E_tl
h2_1_right : X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
Tactic:
simp at h2_1_left
Proof state after:
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_right : X = d.name ∧ xs.length = d.args.length
h2_1_left : d = E_hd ∨ d ∈ E_tl
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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_right : X = d.name ∧ xs.length = d.args.length
h2_1_left : d = E_hd ∨ d ∈ E_tl
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
Tactic:
cases h2_1_left
Proof state after:
case inl
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_right : X = d.name ∧ xs.length = d.args.length
h✝ : d = E_hd
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)

case inr
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_right : X = d.name ∧ xs.length = d.args.length
h✝ : d ∈ E_tl
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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_right : X = d.name ∧ xs.length = d.args.length
c1 : d = E_hd
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
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_right : X = d.name ∧ xs.length = d.args.length
c1 : d = E_hd
⊢ ∃ d ∈ E', X = d.name ∧ xs.length = d.args.length
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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_right : X = d.name ∧ xs.length = d.args.length
c1 : d = E_hd
⊢ ∃ d ∈ E', X = d.name ∧ xs.length = d.args.length
Tactic:
apply Exists.intro E_hd
Proof state after:
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_right : X = d.name ∧ xs.length = d.args.length
c1 : d = E_hd
⊢ E_hd ∈ E' ∧ X = E_hd.name ∧ xs.length = E_hd.args.length
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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_right : X = d.name ∧ xs.length = d.args.length
c1 : d = E_hd
⊢ E_hd ∈ E' ∧ X = E_hd.name ∧ xs.length = E_hd.args.length
Tactic:
simp only [h1_1]
Proof state after:
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_right : X = d.name ∧ xs.length = d.args.length
c1 : d = E_hd
⊢ E_hd ∈ E1 ++ E_hd :: E_tl ∧ X = E_hd.name ∧ xs.length = E_hd.args.length
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
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_right : X = d.name ∧ xs.length = d.args.length
c1 : d = E_hd
⊢ E_hd ∈ E1 ++ E_hd :: E_tl ∧ X = E_hd.name ∧ xs.length = E_hd.args.length
Tactic:
constructor
Proof state after:
case left
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_right : X = d.name ∧ xs.length = d.args.length
c1 : d = E_hd
⊢ E_hd ∈ E1 ++ E_hd :: E_tl

case right
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_right : X = d.name ∧ xs.length = d.args.length
c1 : d = E_hd
⊢ X = E_hd.name ∧ xs.length = E_hd.args.length
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
case left
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_right : X = d.name ∧ xs.length = d.args.length
c1 : d = E_hd
⊢ E_hd ∈ E1 ++ E_hd :: E_tl
Tactic:
simp
Proof state after:
no goals
Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env
Proof state before:
case right
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_right : X = d.name ∧ xs.length = d.args.length
c1 : d = E_hd
⊢ X = E_hd.name ∧ xs.length = E_hd.args.length
Tactic:
simp only [← c1]
Proof state after:
case right
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_right : X = d.name ∧ xs.length = d.args.length
c1 : d = E_hd
⊢ X = d.name ∧ xs.length = d.args.length