internlm/Lean-Github huggingface dataset:
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
case left
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
psi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ psi)
vs : List VarName
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
Tactic:
exact phi_ih vs h1_left
Proof state after:
no goals
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
case right
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
psi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ psi)
vs : List VarName
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ psi)
Tactic:
exact psi_ih vs h1_right
Proof state after:
no goals
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (eq_ x y)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (eq_ x y))
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1 : x ∈ vs ∧ y ∈ vs
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (eq_ x y))
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1 : x ∈ vs ∧ y ∈ vs
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (eq_ x y))
Tactic:
unfold sub
Proof state after:
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1 : x ∈ vs ∧ y ∈ vs
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (eq_ (↑σ x) (↑σ y))
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1 : x ∈ vs ∧ y ∈ vs
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (eq_ (↑σ x) (↑σ y))
Tactic:
unfold NoMetaVarAndAllFreeInList
Proof state after:
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1 : x ∈ vs ∧ y ∈ vs
⊢ ↑σ x ∈ List.map (↑σ) vs ∧ ↑σ y ∈ List.map (↑σ) vs
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1 : x ∈ vs ∧ y ∈ vs
⊢ ↑σ x ∈ List.map (↑σ) vs ∧ ↑σ y ∈ List.map (↑σ) vs
Tactic:
cases h1
Proof state after:
case intro
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
left✝ : x ∈ vs
right✝ : y ∈ vs
⊢ ↑σ x ∈ List.map (↑σ) vs ∧ ↑σ y ∈ List.map (↑σ) vs
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ↑σ x ∈ List.map (↑σ) vs ∧ ↑σ y ∈ List.map (↑σ) vs
Tactic:
constructor
Proof state after:
case left
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ↑σ x ∈ List.map (↑σ) vs

case right
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ↑σ y ∈ List.map (↑σ) vs
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
case left
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ↑σ x ∈ List.map (↑σ) vs
Tactic:
exact List.mem_map_of_mem σ.val h1_left
Proof state after:
no goals
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
case right
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ↑σ y ∈ List.map (↑σ) vs
Tactic:
exact List.mem_map_of_mem σ.val h1_right
Proof state after:
no goals
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (forall_ x phi)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (forall_ x phi))
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (forall_ x phi))
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (forall_ x phi))
Tactic:
unfold sub
Proof state after:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (forall_ (↑σ x) (sub σ τ phi))
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (forall_ (↑σ x) (sub σ τ phi))
Tactic:
unfold NoMetaVarAndAllFreeInList
Proof state after:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ NoMetaVarAndAllFreeInList (↑σ x :: List.map (↑σ) vs) (sub σ τ phi)
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ NoMetaVarAndAllFreeInList (↑σ x :: List.map (↑σ) vs) (sub σ τ phi)
Tactic:
simp only [← List.map_cons]
Proof state after:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) (x :: vs)) (sub σ τ phi)
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) (x :: vs)) (sub σ τ phi)
Tactic:
exact phi_ih (x :: vs) h1
Proof state after:
no goals
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ X xs)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (def_ X xs))
Tactic:
unfold sub
Proof state after:
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ X xs)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (def_ X (List.map (↑σ) xs))
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ X xs)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (def_ X (List.map (↑σ) xs))
Tactic:
unfold NoMetaVarAndAllFreeInList
Proof state after:
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ X xs)
⊢ List.map (↑σ) xs ⊆ List.map (↑σ) vs
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ X xs)
⊢ List.map (↑σ) xs ⊆ List.map (↑σ) vs
Tactic:
exact List.map_subset σ.val h1
Proof state after:
no goals
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
F : Formula
E : Env
σ : Instantiation
h1 : IsMetaVarOrAllDefInEnv E F
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ F)
Tactic:
induction F
Proof state after:
case meta_var_
E : Env
σ : Instantiation
a✝ : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ a✝)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (meta_var_ a✝))

case pred_
E : Env
σ : Instantiation
a✝¹ : PredName
a✝ : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ a✝¹ a✝)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (pred_ a✝¹ a✝))

case eq_
E : Env
σ : Instantiation
a✝¹ a✝ : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ a✝¹ a✝)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (eq_ a✝¹ a✝))

case true_
E : Env
σ : Instantiation
h1 : IsMetaVarOrAllDefInEnv E true_
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ true_)

case not_
E : Env
σ : Instantiation
a✝ : Formula
a_ih✝ : IsMetaVarOrAllDefInEnv E a✝ → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ a✝)
h1 : IsMetaVarOrAllDefInEnv E a✝.not_
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ a✝.not_)

case imp_
E : Env
σ : Instantiation
a✝¹ a✝ : Formula
a_ih✝¹ : IsMetaVarOrAllDefInEnv E a✝¹ → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ a✝¹)
a_ih✝ : IsMetaVarOrAllDefInEnv E a✝ → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ a✝)
h1 : IsMetaVarOrAllDefInEnv E (a✝¹.imp_ a✝)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (a✝¹.imp_ a✝))

case forall_
E : Env
σ : Instantiation
a✝¹ : VarName
a✝ : Formula
a_ih✝ : IsMetaVarOrAllDefInEnv E a✝ → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ a✝)
h1 : IsMetaVarOrAllDefInEnv E (forall_ a✝¹ a✝)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (forall_ a✝¹ a✝))

case def_
E : Env
σ : Instantiation
a✝¹ : DefName
a✝ : List VarName
h1 : IsMetaVarOrAllDefInEnv E (def_ a✝¹ a✝)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (def_ a✝¹ a✝))
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (meta_var_ X))
Tactic:
case meta_var_ X =>
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  simp only
Proof state after:
no goals
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (pred_ X xs))
Tactic:
case pred_ X xs =>
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  simp only
Proof state after:
no goals
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (eq_ x y))
Tactic:
case eq_ x y =>
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  simp only
Proof state after:
no goals
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
h1 : IsMetaVarOrAllDefInEnv E true_
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ true_)
Tactic:
case true_ =>
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  simp only
Proof state after:
no goals
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
h1 : IsMetaVarOrAllDefInEnv E phi.not_
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi.not_)
Tactic:
case not_ phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h1
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  exact phi_ih h1
Proof state after:
no goals
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
h1 : IsMetaVarOrAllDefInEnv E (forall_ x phi)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (forall_ x phi))
Tactic:
case forall_ x phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h1
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  exact phi_ih h1
Proof state after:
no goals
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
X : DefName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (def_ X xs)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (def_ X xs))
Tactic:
case def_ X xs =>
  unfold IsMetaVarOrAllDefInEnv at h1
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  simp
  exact h1
Proof state after:
no goals
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (meta_var_ X))
Tactic:
unfold sub
Proof state after:
E : Env
σ : Instantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
⊢ IsMetaVarOrAllDefInEnv E (meta_var_ X)
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
⊢ IsMetaVarOrAllDefInEnv E (meta_var_ X)
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
E : Env
σ : Instantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
⊢ True
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
⊢ True
Tactic:
simp only
Proof state after:
no goals
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (pred_ X xs))
Tactic:
unfold sub
Proof state after:
E : Env
σ : Instantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ IsMetaVarOrAllDefInEnv E (pred_ X (List.map (↑σ) xs))
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ IsMetaVarOrAllDefInEnv E (pred_ X (List.map (↑σ) xs))
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
E : Env
σ : Instantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ True
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ True
Tactic:
simp only
Proof state after:
no goals
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (eq_ x y))
Tactic:
unfold sub
Proof state after:
E : Env
σ : Instantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ IsMetaVarOrAllDefInEnv E (eq_ (↑σ x) (↑σ y))
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ IsMetaVarOrAllDefInEnv E (eq_ (↑σ x) (↑σ y))
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
E : Env
σ : Instantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ True
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ True
Tactic:
simp only
Proof state after:
no goals
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
h1 : IsMetaVarOrAllDefInEnv E true_
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ true_)
Tactic:
unfold sub
Proof state after:
E : Env
σ : Instantiation
h1 : IsMetaVarOrAllDefInEnv E true_
⊢ IsMetaVarOrAllDefInEnv E true_
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
h1 : IsMetaVarOrAllDefInEnv E true_
⊢ IsMetaVarOrAllDefInEnv E true_
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
E : Env
σ : Instantiation
h1 : IsMetaVarOrAllDefInEnv E true_
⊢ True
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
h1 : IsMetaVarOrAllDefInEnv E true_
⊢ True
Tactic:
simp only
Proof state after:
no goals
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
h1 : IsMetaVarOrAllDefInEnv E phi.not_
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi.not_)
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
Proof state after:
E : Env
σ : Instantiation
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi.not_)
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi.not_)
Tactic:
unfold sub
Proof state after:
E : Env
σ : Instantiation
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi).not_
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi).not_
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
E : Env
σ : Instantiation
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
Tactic:
exact phi_ih h1
Proof state after:
no goals
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
psi_ih : IsMetaVarOrAllDefInEnv E psi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
h1 : IsMetaVarOrAllDefInEnv E (phi.imp_ psi)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (phi.imp_ psi))
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
Proof state after:
E : Env
σ : Instantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
psi_ih : IsMetaVarOrAllDefInEnv E psi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (phi.imp_ psi))
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
psi_ih : IsMetaVarOrAllDefInEnv E psi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (phi.imp_ psi))
Tactic:
unfold sub
Proof state after:
E : Env
σ : Instantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
psi_ih : IsMetaVarOrAllDefInEnv E psi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E ((sub σ meta_var_ phi).imp_ (sub σ meta_var_ psi))
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
psi_ih : IsMetaVarOrAllDefInEnv E psi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E ((sub σ meta_var_ phi).imp_ (sub σ meta_var_ psi))
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
E : Env
σ : Instantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
psi_ih : IsMetaVarOrAllDefInEnv E psi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi) ∧ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
psi_ih : IsMetaVarOrAllDefInEnv E psi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi) ∧ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
Tactic:
cases h1
Proof state after:
case intro
E : Env
σ : Instantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
psi_ih : IsMetaVarOrAllDefInEnv E psi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
left✝ : IsMetaVarOrAllDefInEnv E phi
right✝ : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi) ∧ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
Theorem: MM0.sub_meta_id_preserves_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
σ : Instantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
psi_ih : IsMetaVarOrAllDefInEnv E psi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi) ∧ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
Tactic:
constructor
Proof state after:
case left
E : Env
σ : Instantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
psi_ih : IsMetaVarOrAllDefInEnv E psi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)

case right
E : Env
σ : Instantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
psi_ih : IsMetaVarOrAllDefInEnv E psi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)