internlm/Lean-Github huggingface dataset:
Theorem: MM0.lem_2_a
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (def_ X xs))
Tactic:
unfold sub
Proof state after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E (def_ X (List.map (↑σ) xs))
Theorem: MM0.lem_2_a
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E (def_ X (List.map (↑σ) xs))
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ ∃ d ∈ E, X = d.name ∧ (List.map (↑σ) xs).length = d.args.length
Theorem: MM0.lem_2_a
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ ∃ d ∈ E, X = d.name ∧ (List.map (↑σ) xs).length = d.args.length
Tactic:
simp
Proof state after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
Theorem: MM0.lem_2_a
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
Tactic:
exact h1
Proof state after:
no goals
Theorem: MM0.lem_2_b
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
F : Formula
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ F)
⊢ IsMetaVarOrAllDefInEnv E F
Tactic:
induction F
Proof state after:
case meta_var_
E : Env
σ : Instantiation
τ : MetaInstantiation
a✝ : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (meta_var_ a✝))
⊢ IsMetaVarOrAllDefInEnv E (meta_var_ a✝)

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

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

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

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

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

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

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

case right
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
psi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ psi) → IsMetaVarOrAllDefInEnv E psi
h1_left : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1_right : IsMetaVarOrAllDefInEnv E (sub σ τ psi)
⊢ IsMetaVarOrAllDefInEnv E psi
Theorem: MM0.lem_2_b
Proof state before:
case left
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
psi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ psi) → IsMetaVarOrAllDefInEnv E psi
h1_left : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1_right : IsMetaVarOrAllDefInEnv E (sub σ τ psi)
⊢ IsMetaVarOrAllDefInEnv E phi
Tactic:
exact phi_ih h1_left
Proof state after:
no goals
Theorem: MM0.lem_2_b
Proof state before:
case right
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
psi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ psi) → IsMetaVarOrAllDefInEnv E psi
h1_left : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1_right : IsMetaVarOrAllDefInEnv E (sub σ τ psi)
⊢ IsMetaVarOrAllDefInEnv E psi
Tactic:
exact psi_ih h1_right
Proof state after:
no goals
Theorem: MM0.lem_2_b
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (forall_ x phi))
⊢ IsMetaVarOrAllDefInEnv E (forall_ x phi)
Tactic:
unfold sub at h1
Proof state after:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (forall_ (↑σ x) (sub σ τ phi))
⊢ IsMetaVarOrAllDefInEnv E (forall_ x phi)
Theorem: MM0.lem_2_b
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (forall_ (↑σ x) (sub σ τ phi))
⊢ IsMetaVarOrAllDefInEnv E (forall_ x phi)
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
Proof state after:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
⊢ IsMetaVarOrAllDefInEnv E (forall_ x phi)
Theorem: MM0.lem_2_b
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
⊢ IsMetaVarOrAllDefInEnv E (forall_ x phi)
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
⊢ IsMetaVarOrAllDefInEnv E phi
Theorem: MM0.lem_2_b
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
⊢ IsMetaVarOrAllDefInEnv E phi
Tactic:
exact phi_ih h1
Proof state after:
no goals
Theorem: MM0.lem_2_b
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (def_ X xs))
⊢ IsMetaVarOrAllDefInEnv E (def_ X xs)
Tactic:
unfold sub at h1
Proof state after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (def_ X (List.map (↑σ) xs))
⊢ IsMetaVarOrAllDefInEnv E (def_ X xs)
Theorem: MM0.lem_2_b
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (def_ X (List.map (↑σ) xs))
⊢ IsMetaVarOrAllDefInEnv E (def_ X xs)
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
Proof state after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : ∃ d ∈ E, X = d.name ∧ (List.map (↑σ) xs).length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E (def_ X xs)
Theorem: MM0.lem_2_b
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : ∃ d ∈ E, X = d.name ∧ (List.map (↑σ) xs).length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E (def_ X xs)
Tactic:
simp at h1
Proof state after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E (def_ X xs)
Theorem: MM0.lem_2_b
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E (def_ X xs)
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
Theorem: MM0.lem_2_b
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
Tactic:
exact h1
Proof state after:
no goals
Theorem: MM0.is_proof_imp_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : h1_phi ∈ h1_Δ
⊢ IsMetaVarOrAllDefInEnv E h1_phi
Tactic:
case hyp h1_Γ h1_Δ h1_phi h1_1 h1_2 =>
  exact h1_1
Proof state after:
no goals
Theorem: MM0.is_proof_imp_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsProof E h1_Γ h1_Δ h1_phi
h1_2 : IsProof E h1_Γ h1_Δ (h1_phi.imp_ h1_psi)
h1_ih_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_ih_2 : IsMetaVarOrAllDefInEnv E (h1_phi.imp_ h1_psi)
⊢ IsMetaVarOrAllDefInEnv E h1_psi
Tactic:
case mp h1_Γ h1_Δ h1_phi h1_psi h1_1 h1_2 h1_ih_1 h1_ih_2 =>
  unfold IsMetaVarOrAllDefInEnv at h1_ih_2
  cases h1_ih_2
  case intro h1_ih_2_left h1_ih_2_right =>
    exact h1_ih_2_right
Proof state after:
no goals
Theorem: MM0.is_proof_imp_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
⊢ IsMetaVarOrAllDefInEnv E (h1_phi.imp_ (h1_psi.imp_ h1_phi))
Tactic:
case prop_1 h1_Γ h1_Δ h1_phi h1_psi h1_1 h1_2 =>
  repeat first | constructor | assumption
Proof state after:
no goals
Theorem: MM0.is_proof_imp_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi h1_chi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
h1_3 : IsMetaVarOrAllDefInEnv E h1_chi
⊢ IsMetaVarOrAllDefInEnv E ((h1_phi.imp_ (h1_psi.imp_ h1_chi)).imp_ ((h1_phi.imp_ h1_psi).imp_ (h1_phi.imp_ h1_chi)))
Tactic:
case prop_2 h1_Γ h1_Δ h1_phi h1_psi h1_chi h1_1 h1_2 h1_3 =>
  repeat first | constructor | assumption
Proof state after:
no goals
Theorem: MM0.is_proof_imp_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
⊢ IsMetaVarOrAllDefInEnv E ((h1_phi.not_.imp_ h1_psi.not_).imp_ (h1_psi.imp_ h1_phi))
Tactic:
case prop_3 h1_Γ h1_Δ h1_phi h1_psi h1_1 h1_2 =>
  repeat first | constructor | assumption
Proof state after:
no goals
Theorem: MM0.is_proof_imp_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi : Formula
h1_x : VarName
h1_1 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih : IsMetaVarOrAllDefInEnv E h1_phi
⊢ IsMetaVarOrAllDefInEnv E (forall_ h1_x h1_phi)
Tactic:
case gen h1_Γ h1_Δ h1_phi h1_x h1_1 h1_ih =>
  repeat first | constructor | assumption
Proof state after:
no goals
Theorem: MM0.is_proof_imp_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
⊢ IsMetaVarOrAllDefInEnv E ((forall_ h1_x (h1_phi.imp_ h1_psi)).imp_ ((forall_ h1_x h1_phi).imp_ (forall_ h1_x h1_psi)))
Tactic:
case pred_1 h1_Γ h1_Δ h1_phi h1_psi h1_x h1_1 h1_2 =>
  repeat first | constructor | assumption
Proof state after:
no goals
Theorem: MM0.is_proof_imp_is_meta_var_or_all_def_in_env
Proof state before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x h1_phi
⊢ IsMetaVarOrAllDefInEnv E (h1_phi.imp_ (forall_ h1_x h1_phi))
Tactic:
case pred_2 h1_Γ h1_Δ h1_phi h1_x h1_1 h1_2 =>
  repeat first | constructor | assumption
Proof state after:
no goals