internlm/Lean-Github huggingface dataset:
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
case h.e'_1
σ : Instantiation
τ τ' : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ sub σ τ phi = sub σ τ' phi
Tactic:
exact phi_ih h1
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1 : (phi.imp_ psi).metaVarSet = ∅
⊢ sub σ τ (phi.imp_ psi) = sub σ τ' (phi.imp_ psi)
Tactic:
unfold Formula.metaVarSet at h1
Proof state after:
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1 : phi.metaVarSet ∪ psi.metaVarSet = ∅
⊢ sub σ τ (phi.imp_ psi) = sub σ τ' (phi.imp_ psi)
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1 : phi.metaVarSet ∪ psi.metaVarSet = ∅
⊢ sub σ τ (phi.imp_ psi) = sub σ τ' (phi.imp_ psi)
Tactic:
simp only [Finset.union_eq_empty] at h1
Proof state after:
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1 : phi.metaVarSet = ∅ ∧ psi.metaVarSet = ∅
⊢ sub σ τ (phi.imp_ psi) = sub σ τ' (phi.imp_ psi)
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1 : phi.metaVarSet = ∅ ∧ psi.metaVarSet = ∅
⊢ sub σ τ (phi.imp_ psi) = sub σ τ' (phi.imp_ psi)
Tactic:
unfold sub
Proof state after:
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1 : phi.metaVarSet = ∅ ∧ psi.metaVarSet = ∅
⊢ (sub σ τ phi).imp_ (sub σ τ psi) = (sub σ τ' phi).imp_ (sub σ τ' psi)
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1 : phi.metaVarSet = ∅ ∧ psi.metaVarSet = ∅
⊢ (sub σ τ phi).imp_ (sub σ τ psi) = (sub σ τ' phi).imp_ (sub σ τ' psi)
Tactic:
cases h1
Proof state after:
case intro
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
left✝ : phi.metaVarSet = ∅
right✝ : psi.metaVarSet = ∅
⊢ (sub σ τ phi).imp_ (sub σ τ psi) = (sub σ τ' phi).imp_ (sub σ τ' psi)
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ (sub σ τ phi).imp_ (sub σ τ psi) = (sub σ τ' phi).imp_ (sub σ τ' psi)
Tactic:
congr! 1
Proof state after:
case h.e'_1
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ sub σ τ phi = sub σ τ' phi

case h.e'_2
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ sub σ τ psi = sub σ τ' psi
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
case h.e'_1
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ sub σ τ phi = sub σ τ' phi
Tactic:
exact phi_ih h1_left
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
case h.e'_2
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ sub σ τ psi = sub σ τ' psi
Tactic:
exact psi_ih h1_right
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : (forall_ x phi).metaVarSet = ∅
⊢ sub σ τ (forall_ x phi) = sub σ τ' (forall_ x phi)
Tactic:
unfold Formula.metaVarSet at h1
Proof state after:
σ : Instantiation
τ τ' : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ sub σ τ (forall_ x phi) = sub σ τ' (forall_ x phi)
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ sub σ τ (forall_ x phi) = sub σ τ' (forall_ x phi)
Tactic:
unfold sub
Proof state after:
σ : Instantiation
τ τ' : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ forall_ (↑σ x) (sub σ τ phi) = forall_ (↑σ x) (sub σ τ' phi)
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ forall_ (↑σ x) (sub σ τ phi) = forall_ (↑σ x) (sub σ τ' phi)
Tactic:
congr! 1
Proof state after:
case h.e'_2
σ : Instantiation
τ τ' : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ sub σ τ phi = sub σ τ' phi
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
case h.e'_2
σ : Instantiation
τ τ' : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ sub σ τ phi = sub σ τ' phi
Tactic:
exact phi_ih h1
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
X : DefName
xs : List VarName
h1 : (def_ X xs).metaVarSet = ∅
⊢ sub σ τ (def_ X xs) = sub σ τ' (def_ X xs)
Tactic:
rfl
Proof state after:
no goals
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
F : Formula
vs : List VarName
σ : Instantiation
τ : MetaInstantiation
h1 : NoMetaVarAndAllFreeInList vs F
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ F)
Tactic:
induction F generalizing vs
Proof state after:
case meta_var_
σ : Instantiation
τ : MetaInstantiation
a✝ : MetaVarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ a✝)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (meta_var_ a✝))

case pred_
σ : Instantiation
τ : MetaInstantiation
a✝¹ : PredName
a✝ vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ a✝¹ a✝)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (pred_ a✝¹ a✝))

case eq_
σ : Instantiation
τ : MetaInstantiation
a✝¹ a✝ : VarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (eq_ a✝¹ a✝)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (eq_ a✝¹ a✝))

case true_
σ : Instantiation
τ : MetaInstantiation
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ true_)

case not_
σ : Instantiation
τ : MetaInstantiation
a✝ : Formula
a_ih✝ :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ a✝)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs a✝.not_
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ a✝.not_)

case imp_
σ : Instantiation
τ : MetaInstantiation
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝¹ → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ a✝¹)
a_ih✝ :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ a✝)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (a✝¹.imp_ a✝)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (a✝¹.imp_ a✝))

case forall_
σ : Instantiation
τ : MetaInstantiation
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ a✝)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (forall_ a✝¹ a✝)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (forall_ a✝¹ a✝))

case def_
σ : Instantiation
τ : MetaInstantiation
a✝¹ : DefName
a✝ vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ a✝¹ a✝)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (def_ a✝¹ a✝))
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ X)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (meta_var_ X))
Tactic:
case meta_var_ X =>
  unfold NoMetaVarAndAllFreeInList at h1
  contradiction
Proof state after:
no goals
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ X xs)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (pred_ X xs))
Tactic:
case pred_ X xs =>
  unfold sub
  unfold NoMetaVarAndAllFreeInList
  exact List.map_subset σ.1 h1
Proof state after:
no goals
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ true_)
Tactic:
case true_ =>
  unfold sub
  unfold NoMetaVarAndAllFreeInList
  simp
Proof state after:
no goals
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi.not_
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi.not_)
Tactic:
case not_ phi phi_ih =>
  unfold NoMetaVarAndAllFreeInList at h1
  unfold sub
  unfold NoMetaVarAndAllFreeInList
  exact phi_ih 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 : 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:
case forall_ x phi phi_ih =>
  unfold NoMetaVarAndAllFreeInList at h1
  unfold sub
  unfold NoMetaVarAndAllFreeInList
  simp only [← List.map_cons]
  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:
case def_ X xs =>
  unfold sub
  unfold NoMetaVarAndAllFreeInList
  exact List.map_subset σ.val h1
Proof state after:
no goals
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ X)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (meta_var_ X))
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
vs : List VarName
h1 : False
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (meta_var_ X))
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
vs : List VarName
h1 : False
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (meta_var_ X))
Tactic:
contradiction
Proof state after:
no goals
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ X xs)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (pred_ X xs))
Tactic:
unfold sub
Proof state after:
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ X xs)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (pred_ X (List.map (↑σ) xs))
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ X xs)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (pred_ X (List.map (↑σ) xs))
Tactic:
unfold NoMetaVarAndAllFreeInList
Proof state after:
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ 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 : PredName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ X xs)
⊢ List.map (↑σ) xs ⊆ List.map (↑σ) vs
Tactic:
exact List.map_subset σ.1 h1
Proof state after:
no goals
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ true_)
Tactic:
unfold sub
Proof state after:
σ : Instantiation
τ : MetaInstantiation
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) true_
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) true_
Tactic:
unfold NoMetaVarAndAllFreeInList
Proof state after:
σ : Instantiation
τ : MetaInstantiation
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
⊢ True
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
⊢ True
Tactic:
simp
Proof state after:
no goals
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi.not_
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi.not_)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi.not_)
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi.not_)
Tactic:
unfold sub
Proof state after:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi).not_
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi).not_
Tactic:
unfold NoMetaVarAndAllFreeInList
Proof state after:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi)
Tactic:
exact phi_ih vs h1
Proof state after:
no goals
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : 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 : NoMetaVarAndAllFreeInList vs (phi.imp_ psi)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (phi.imp_ psi))
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
σ : 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 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (phi.imp_ psi))
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : 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 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (phi.imp_ psi))
Tactic:
unfold sub
Proof state after:
σ : 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 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) ((sub σ τ phi).imp_ (sub σ τ psi))
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : 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 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) ((sub σ τ phi).imp_ (sub σ τ psi))
Tactic:
unfold NoMetaVarAndAllFreeInList
Proof state after:
σ : 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 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi) ∧
    NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ psi)
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : 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 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi) ∧
    NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ psi)
Tactic:
cases h1
Proof state after:
case intro
σ : 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
left✝ : NoMetaVarAndAllFreeInList vs phi
right✝ : NoMetaVarAndAllFreeInList vs psi
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ phi) ∧
    NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ psi)
Theorem: MM0.no_meta_var_and_all_free_in_list_map_sub
Proof state before:
σ : 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) ∧
    NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ psi)
Tactic:
constructor
Proof state after:
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)

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)