internlm/Lean-Github huggingface dataset:
Theorem: MM0.lem_2_a
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ X ∈ (phi.imp_ psi).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (phi.imp_ psi))
Tactic:
unfold Formula.metaVarSet at h2
Proof state after:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
h2 : ∀ X ∈ phi.metaVarSet ∪ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (phi.imp_ psi))
Theorem: MM0.lem_2_a
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
h2 : ∀ X ∈ phi.metaVarSet ∪ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (phi.imp_ psi))
Tactic:
simp at h2
Proof state after:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (phi.imp_ psi))
Theorem: MM0.lem_2_a
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (phi.imp_ psi))
Tactic:
unfold sub
Proof state after:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E ((sub σ τ phi).imp_ (sub σ τ psi))
Theorem: MM0.lem_2_a
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E ((sub σ τ phi).imp_ (sub σ τ psi))
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi) ∧ IsMetaVarOrAllDefInEnv E (sub σ τ psi)
Theorem: MM0.lem_2_a
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi) ∧ IsMetaVarOrAllDefInEnv E (sub σ τ psi)
Tactic:
cases h1
Proof state after:
case intro
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
left✝ : IsMetaVarOrAllDefInEnv E phi
right✝ : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi) ∧ IsMetaVarOrAllDefInEnv E (sub σ τ psi)
Theorem: MM0.lem_2_a
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi) ∧ IsMetaVarOrAllDefInEnv E (sub σ τ psi)
Tactic:
constructor
Proof state after:
case left
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi)

case right
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ psi)
Theorem: MM0.lem_2_a
Proof state before:
case left
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi)
Tactic:
apply phi_ih h1_left
Proof state after:
case left
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
Theorem: MM0.lem_2_a
Proof state before:
case left
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
Tactic:
intro X a1
Proof state after:
case left
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ phi.metaVarSet
⊢ IsMetaVarOrAllDefInEnv E (τ X)
Theorem: MM0.lem_2_a
Proof state before:
case left
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ phi.metaVarSet
⊢ IsMetaVarOrAllDefInEnv E (τ X)
Tactic:
apply h2
Proof state after:
case left.a
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ phi.metaVarSet
⊢ X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet
Theorem: MM0.lem_2_a
Proof state before:
case left.a
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ phi.metaVarSet
⊢ X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet
Tactic:
left
Proof state after:
case left.a.h
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ phi.metaVarSet
⊢ X ∈ phi.metaVarSet
Theorem: MM0.lem_2_a
Proof state before:
case left.a.h
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ phi.metaVarSet
⊢ X ∈ phi.metaVarSet
Tactic:
exact a1
Proof state after:
no goals
Theorem: MM0.lem_2_a
Proof state before:
case right
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ psi)
Tactic:
apply psi_ih h1_right
Proof state after:
case right
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ ∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
Theorem: MM0.lem_2_a
Proof state before:
case right
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ ∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
Tactic:
intro X a1
Proof state after:
case right
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ IsMetaVarOrAllDefInEnv E (τ X)
Theorem: MM0.lem_2_a
Proof state before:
case right
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ IsMetaVarOrAllDefInEnv E (τ X)
Tactic:
apply h2
Proof state after:
case right.a
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet
Theorem: MM0.lem_2_a
Proof state before:
case right.a
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet
Tactic:
right
Proof state after:
case right.a.h
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ X ∈ psi.metaVarSet
Theorem: MM0.lem_2_a
Proof state before:
case right.a.h
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
X : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ X ∈ psi.metaVarSet
Tactic:
exact a1
Proof state after:
no goals
Theorem: MM0.lem_2_a
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E (forall_ x phi)
h2 : ∀ X ∈ (forall_ x phi).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (forall_ x phi))
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
Proof state after:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h2 : ∀ X ∈ (forall_ x phi).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (forall_ x phi))
Theorem: MM0.lem_2_a
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h2 : ∀ X ∈ (forall_ x phi).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (forall_ x phi))
Tactic:
unfold Formula.metaVarSet at h2
Proof state after:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (forall_ x phi))
Theorem: MM0.lem_2_a
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (forall_ x phi))
Tactic:
unfold sub
Proof state after:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (forall_ (↑σ x) (sub σ τ phi))
Theorem: MM0.lem_2_a
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (forall_ (↑σ x) (sub σ τ phi))
Tactic:
unfold IsMetaVarOrAllDefInEnv
Proof state after:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi)
Theorem: MM0.lem_2_a
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi)
Tactic:
exact phi_ih h1 h2
Proof state after:
no goals
Theorem: MM0.lem_2_a
Proof state before:
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (def_ X xs)
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (def_ X xs))
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
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 (sub σ τ (def_ X xs))