Theorem: MM0.concat_env_preserves_is_meta_var_or_all_def_in_env (FOL/MM0/MM0.lean)

State before:
E E' : Env
F : Formula
h1 : ∃ E1, E' = E1 ++ E
h2 : IsMetaVarOrAllDefInEnv E F
⊢ IsMetaVarOrAllDefInEnv E' F
Tactic:
induction E generalizing F
State after:
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

State before:
E' : Env
h1 : ∃ E1, E' = E1 ++ []
X : DefName
xs : List VarName
h2 : IsMetaVarOrAllDefInEnv [] (def_ X xs)
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
Tactic:
case nil.def_ X xs =>
  unfold IsMetaVarOrAllDefInEnv at h2
  simp at h2
State after:
no goals

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
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✝)

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 : MetaVarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (meta_var_ X)
⊢ IsMetaVarOrAllDefInEnv E' (meta_var_ X)
Tactic:
case meta_var_ X =>
  unfold IsMetaVarOrAllDefInEnv
  simp only
State after:
no goals

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 : PredName
xs : List VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (pred_ X xs)
⊢ IsMetaVarOrAllDefInEnv E' (pred_ X xs)
Tactic:
case pred_ X xs =>
  unfold IsMetaVarOrAllDefInEnv
  simp only
State after:
no goals

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

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✝
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) true_
⊢ IsMetaVarOrAllDefInEnv E' true_
Tactic:
case true_ =>
  unfold IsMetaVarOrAllDefInEnv
  simp only
State after:
no goals

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 : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi.not_
⊢ IsMetaVarOrAllDefInEnv E' phi.not_
Tactic:
case not_ phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h2
  unfold IsMetaVarOrAllDefInEnv
  exact phi_ih h2
State after:
no goals

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:
case forall_ x phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h2
  unfold IsMetaVarOrAllDefInEnv
  exact phi_ih h2
State after:
no goals

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 : MetaVarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (meta_var_ X)
⊢ IsMetaVarOrAllDefInEnv E' (meta_var_ X)
Tactic:
unfold IsMetaVarOrAllDefInEnv
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 : MetaVarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (meta_var_ X)
⊢ True

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 : MetaVarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (meta_var_ X)
⊢ True
Tactic:
simp only
State after:
no goals

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 : PredName
xs : List VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (pred_ X xs)
⊢ IsMetaVarOrAllDefInEnv E' (pred_ X xs)
Tactic:
unfold IsMetaVarOrAllDefInEnv
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 : PredName
xs : List VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (pred_ X xs)
⊢ True

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 : PredName
xs : List VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (pred_ X xs)
⊢ True
Tactic:
simp only
State after:
no goals

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 y : VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (eq_ x y)
⊢ IsMetaVarOrAllDefInEnv E' (eq_ x y)
Tactic:
unfold IsMetaVarOrAllDefInEnv
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 y : VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (eq_ x y)
⊢ True

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 y : VarName
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (eq_ x y)
⊢ True
Tactic:
simp only
State after:
no goals

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✝
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) true_
⊢ IsMetaVarOrAllDefInEnv E' true_
Tactic:
unfold IsMetaVarOrAllDefInEnv
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✝
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) true_
⊢ True

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✝
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) true_
⊢ True
Tactic:
simp only
State after:
no goals

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 : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi.not_
⊢ IsMetaVarOrAllDefInEnv E' phi.not_
Tactic:
unfold IsMetaVarOrAllDefInEnv at h2
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 : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi
⊢ IsMetaVarOrAllDefInEnv E' phi.not_

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 : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi
⊢ IsMetaVarOrAllDefInEnv E' phi.not_
Tactic:
unfold IsMetaVarOrAllDefInEnv
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 : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi
⊢ IsMetaVarOrAllDefInEnv E' phi

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 : Formula
phi_ih : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi → IsMetaVarOrAllDefInEnv E' phi
h2 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) phi
⊢ IsMetaVarOrAllDefInEnv E' phi
Tactic:
exact phi_ih h2
State after:
no goals

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
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)

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
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
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)

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
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

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
State after:
no goals

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
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)

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
State after:
no goals

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
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)

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
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)

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
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)

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
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)

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
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)

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
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)

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
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)

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
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)

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
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

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
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

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]
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

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
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

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
State after:
no goals

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]
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

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 = d.name ∧ xs.length = d.args.length
Tactic:
exact h2_1_right
State after:
no goals

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_tl
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
Tactic:
apply E_ih
State after:
case h1
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_tl
⊢ ∃ E1, E' = E1 ++ E_tl

case h2
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_tl
⊢ IsMetaVarOrAllDefInEnv E_tl (def_ X xs)

State before:
case h1
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_tl
⊢ ∃ E1, E' = E1 ++ E_tl
Tactic:
apply Exists.intro (E1 ++ [E_hd])
State after:
case h1
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_tl
⊢ E' = E1 ++ [E_hd] ++ E_tl

State before:
case h1
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_tl
⊢ E' = E1 ++ [E_hd] ++ E_tl
Tactic:
simp
State after:
case h1
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_tl
⊢ E' = E1 ++ E_hd :: E_tl

State before:
case h1
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_tl
⊢ E' = E1 ++ E_hd :: E_tl
Tactic:
exact h1_1
State after:
no goals

State before:
case h2
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_tl
⊢ IsMetaVarOrAllDefInEnv E_tl (def_ X xs)
Tactic:
unfold IsMetaVarOrAllDefInEnv
State after:
case h2
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_tl
⊢ ∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length

State before:
case h2
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_tl
⊢ ∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length
Tactic:
apply Exists.intro d
State after:
case h2
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_tl
⊢ d ∈ E_tl ∧ X = d.name ∧ xs.length = d.args.length

State before:
case h2
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_tl
⊢ d ∈ E_tl ∧ X = d.name ∧ xs.length = d.args.length
Tactic:
constructor
State after:
case h2.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_tl
⊢ d ∈ E_tl

case h2.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_tl
⊢ X = d.name ∧ xs.length = d.args.length

State before:
case h2.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_tl
⊢ d ∈ E_tl
Tactic:
exact c1
State after:
no goals

State before:
case h2.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_tl
⊢ X = d.name ∧ xs.length = d.args.length
Tactic:
exact h2_1_right
State after:
no goals