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

State before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1 : IsProof E Γ Δ F
⊢ IsMetaVarOrAllDefInEnv E F
Tactic:
induction h1
State after:
case hyp
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
phi✝ : Formula
a✝¹ : IsMetaVarOrAllDefInEnv E phi✝
a✝ : phi✝ ∈ Δ✝
⊢ IsMetaVarOrAllDefInEnv E phi✝

case mp
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
phi✝ psi✝ : Formula
a✝¹ : IsProof E Γ✝ Δ✝ phi✝
a✝ : IsProof E Γ✝ Δ✝ (phi✝.imp_ psi✝)
a_ih✝¹ : IsMetaVarOrAllDefInEnv E phi✝
a_ih✝ : IsMetaVarOrAllDefInEnv E (phi✝.imp_ psi✝)
⊢ IsMetaVarOrAllDefInEnv E psi✝

case prop_1
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
phi✝ psi✝ : Formula
a✝¹ : IsMetaVarOrAllDefInEnv E phi✝
a✝ : IsMetaVarOrAllDefInEnv E psi✝
⊢ IsMetaVarOrAllDefInEnv E (phi✝.imp_ (psi✝.imp_ phi✝))

case prop_2
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
phi✝ psi✝ chi✝ : Formula
a✝² : IsMetaVarOrAllDefInEnv E phi✝
a✝¹ : IsMetaVarOrAllDefInEnv E psi✝
a✝ : IsMetaVarOrAllDefInEnv E chi✝
⊢ IsMetaVarOrAllDefInEnv E ((phi✝.imp_ (psi✝.imp_ chi✝)).imp_ ((phi✝.imp_ psi✝).imp_ (phi✝.imp_ chi✝)))

case prop_3
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
phi✝ psi✝ : Formula
a✝¹ : IsMetaVarOrAllDefInEnv E phi✝
a✝ : IsMetaVarOrAllDefInEnv E psi✝
⊢ IsMetaVarOrAllDefInEnv E ((phi✝.not_.imp_ psi✝.not_).imp_ (psi✝.imp_ phi✝))

case gen
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
phi✝ : Formula
x✝ : VarName
a✝ : IsProof E Γ✝ Δ✝ phi✝
a_ih✝ : IsMetaVarOrAllDefInEnv E phi✝
⊢ IsMetaVarOrAllDefInEnv E (forall_ x✝ phi✝)

case pred_1
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
phi✝ psi✝ : Formula
x✝ : VarName
a✝¹ : IsMetaVarOrAllDefInEnv E phi✝
a✝ : IsMetaVarOrAllDefInEnv E psi✝
⊢ IsMetaVarOrAllDefInEnv E ((forall_ x✝ (phi✝.imp_ psi✝)).imp_ ((forall_ x✝ phi✝).imp_ (forall_ x✝ psi✝)))

case pred_2
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
phi✝ : Formula
x✝ : VarName
a✝¹ : IsMetaVarOrAllDefInEnv E phi✝
a✝ : NotFree Γ✝ x✝ phi✝
⊢ IsMetaVarOrAllDefInEnv E (phi✝.imp_ (forall_ x✝ phi✝))

case eq_1
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
x✝ y✝ : VarName
a✝ : ¬y✝ = x✝
⊢ IsMetaVarOrAllDefInEnv E (exists_ x✝ (eq_ x✝ y✝))

case eq_2
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
x✝ y✝ z✝ : VarName
⊢ IsMetaVarOrAllDefInEnv E ((eq_ x✝ y✝).imp_ ((eq_ x✝ z✝).imp_ (eq_ y✝ z✝)))

case eq_3
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
n✝ : ℕ
name✝ : PredName
xs✝ ys✝ : Fin n✝ → VarName
⊢ IsMetaVarOrAllDefInEnv E (eqSubPred name✝ n✝ xs✝ ys✝)

case thm
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
Γ✝ Γ'✝ : List (VarName × MetaVarName)
Δ✝ Δ'✝ : List Formula
phi✝ : Formula
σ✝ : Instantiation
τ✝ : MetaInstantiation
a✝³ : ∀ X ∈ phi✝.metaVarSet, IsMetaVarOrAllDefInEnv E (τ✝ X)
a✝² : ∀ (x : VarName) (X : MetaVarName), (x, X) ∈ Γ✝ → NotFree Γ'✝ (↑σ✝ x) (τ✝ X)
a✝¹ : ∀ psi ∈ Δ✝, IsProof E Γ'✝ Δ'✝ (sub σ✝ τ✝ psi)
a✝ : IsProof E Γ✝ Δ✝ phi✝
a_ih✝¹ : ∀ psi ∈ Δ✝, IsMetaVarOrAllDefInEnv E (sub σ✝ τ✝ psi)
a_ih✝ : IsMetaVarOrAllDefInEnv E phi✝
⊢ IsMetaVarOrAllDefInEnv E (sub σ✝ τ✝ phi✝)

case conv
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
phi✝ phi'✝ : Formula
a✝² : IsMetaVarOrAllDefInEnv E phi'✝
a✝¹ : IsProof E Γ✝ Δ✝ phi✝
a✝ : IsConv E phi✝ phi'✝
a_ih✝ : IsMetaVarOrAllDefInEnv E phi✝
⊢ IsMetaVarOrAllDefInEnv E phi'✝

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

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

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

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

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

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

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

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

State before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
⊢ IsMetaVarOrAllDefInEnv E (exists_ h1_x (eq_ h1_x h1_y))
Tactic:
case eq_1 h1_Γ h1_Δ h1_x h1_y h1_1 =>
  unfold exists_
  repeat first | constructor | assumption
State after:
no goals

State before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
⊢ IsMetaVarOrAllDefInEnv E ((eq_ h1_x h1_y).imp_ ((eq_ h1_x h1_z).imp_ (eq_ h1_y h1_z)))
Tactic:
case eq_2 h1_Γ h1_Δ h1_x h1_y h1_z =>
  unfold IsMetaVarOrAllDefInEnv
  repeat first | constructor | assumption
State after:
no goals

State before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_n : ℕ
h1_name : PredName
h1_xs h1_ys : Fin h1_n → VarName
⊢ IsMetaVarOrAllDefInEnv E (eqSubPred h1_name h1_n h1_xs h1_ys)
Tactic:
case eq_3 h1_Γ h1_Δ h1_n h1_name h1_xs h1_ys =>
  sorry
State after:
no goals

State before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ h1_Γ' : List (VarName × MetaVarName)
h1_Δ h1_Δ' : List Formula
h1_phi : Formula
h1_σ : Instantiation
h1_τ : MetaInstantiation
h1_1 : ∀ X ∈ h1_phi.metaVarSet, IsMetaVarOrAllDefInEnv E (h1_τ X)
h1_2 : ∀ (x : VarName) (X : MetaVarName), (x, X) ∈ h1_Γ → NotFree h1_Γ' (↑h1_σ x) (h1_τ X)
h1_3 : ∀ psi ∈ h1_Δ, IsProof E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)
h1_4 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih_1 : ∀ psi ∈ h1_Δ, IsMetaVarOrAllDefInEnv E (sub h1_σ h1_τ psi)
h1_ih_2 : IsMetaVarOrAllDefInEnv E h1_phi
⊢ IsMetaVarOrAllDefInEnv E (sub h1_σ h1_τ h1_phi)
Tactic:
case thm h1_Γ h1_Γ' h1_Δ h1_Δ' h1_phi h1_σ h1_τ h1_1 h1_2 h1_3 h1_4 h1_ih_1 h1_ih_2 =>
  exact lem_2_a E h1_σ h1_τ h1_phi h1_ih_2 h1_1
State after:
no goals

State before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_phi' : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi'
h1_2 : IsProof E h1_Γ h1_Δ h1_phi
h1_3 : IsConv E h1_phi h1_phi'
h1_ih : IsMetaVarOrAllDefInEnv E h1_phi
⊢ IsMetaVarOrAllDefInEnv E h1_phi'
Tactic:
case conv h1_Γ h1_Δ h1_phi h1_phi' h1_1 h1_2 h1_3 h1_ih =>
  exact h1_1
State after:
no goals

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

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:
unfold IsMetaVarOrAllDefInEnv at h1_ih_2
State after:
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 ∧ IsMetaVarOrAllDefInEnv E h1_psi
⊢ IsMetaVarOrAllDefInEnv E h1_psi

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 ∧ IsMetaVarOrAllDefInEnv E h1_psi
⊢ IsMetaVarOrAllDefInEnv E h1_psi
Tactic:
cases h1_ih_2
State after:
case intro
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 left✝ : IsMetaVarOrAllDefInEnv E h1_phi
right✝ : IsMetaVarOrAllDefInEnv E h1_psi
⊢ IsMetaVarOrAllDefInEnv E h1_psi

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 h1_ih_2_left : IsMetaVarOrAllDefInEnv E h1_phi
h1_ih_2_right : IsMetaVarOrAllDefInEnv E h1_psi
⊢ IsMetaVarOrAllDefInEnv E h1_psi
Tactic:
case intro h1_ih_2_left h1_ih_2_right =>
  exact h1_ih_2_right
State after:
no goals

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 h1_ih_2_left : IsMetaVarOrAllDefInEnv E h1_phi
h1_ih_2_right : IsMetaVarOrAllDefInEnv E h1_psi
⊢ IsMetaVarOrAllDefInEnv E h1_psi
Tactic:
exact h1_ih_2_right
State after:
no goals

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:
repeat first | constructor | assumption
State after:
no goals

State before:
case right.right
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
Tactic:
first | constructor | assumption
State after:
no goals

State before:
case right
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_psi.imp_ h1_phi)
Tactic:
constructor
State after:
case right.left
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_psi

case right.right
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

State before:
case right.right
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
Tactic:
assumption
State after:
no goals

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:
repeat first | constructor | assumption
State after:
no goals

State before:
case right.right.right
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_chi
Tactic:
first | constructor | assumption
State after:
no goals

State before:
case right.right
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_chi)
Tactic:
constructor
State after:
case right.right.left
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

case right.right.right
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_chi

State before:
case right.right.right
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_chi
Tactic:
assumption
State after:
no goals

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:
repeat first | constructor | assumption
State after:
no goals

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:
repeat first | constructor | assumption
State after:
no goals

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

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

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:
repeat first | constructor | assumption
State after:
no goals

State before:
case right.right
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_psi)
Tactic:
first | constructor | assumption
State after:
no goals

State before:
case right
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_ (forall_ h1_x h1_psi))
Tactic:
constructor
State after:
case right.left
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)

case right.right
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_psi)

State before:
case right.right
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_psi)
Tactic:
assumption
State after:
no goals

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:
repeat first | constructor | assumption
State after:
no goals

State before:
case right
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 (forall_ h1_x h1_phi)
Tactic:
first | constructor | assumption
State after:
no goals

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:
constructor
State after:
case left
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

case right
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 (forall_ h1_x h1_phi)

State before:
case right
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 (forall_ h1_x h1_phi)
Tactic:
assumption
State after:
no goals

State before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
⊢ IsMetaVarOrAllDefInEnv E (exists_ h1_x (eq_ h1_x h1_y))
Tactic:
unfold exists_
State after:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
⊢ IsMetaVarOrAllDefInEnv E (forall_ h1_x (eq_ h1_x h1_y).not_).not_

State before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
⊢ IsMetaVarOrAllDefInEnv E (forall_ h1_x (eq_ h1_x h1_y).not_).not_
Tactic:
repeat first | constructor | assumption
State after:
no goals

State before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
⊢ IsMetaVarOrAllDefInEnv E (forall_ h1_x (eq_ h1_x h1_y).not_).not_
Tactic:
first | constructor | assumption
State after:
no goals

State before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
⊢ IsMetaVarOrAllDefInEnv E (forall_ h1_x (eq_ h1_x h1_y).not_).not_
Tactic:
constructor
State after:
no goals

State before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
⊢ IsMetaVarOrAllDefInEnv E ((eq_ h1_x h1_y).imp_ ((eq_ h1_x h1_z).imp_ (eq_ h1_y h1_z)))
Tactic:
unfold IsMetaVarOrAllDefInEnv
State after:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
⊢ IsMetaVarOrAllDefInEnv E (eq_ h1_x h1_y) ∧ IsMetaVarOrAllDefInEnv E ((eq_ h1_x h1_z).imp_ (eq_ h1_y h1_z))

State before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
⊢ IsMetaVarOrAllDefInEnv E (eq_ h1_x h1_y) ∧ IsMetaVarOrAllDefInEnv E ((eq_ h1_x h1_z).imp_ (eq_ h1_y h1_z))
Tactic:
repeat first | constructor | assumption
State after:
no goals

State before:
case right.right
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
⊢ IsMetaVarOrAllDefInEnv E (eq_ h1_y h1_z)
Tactic:
first | constructor | assumption
State after:
no goals

State before:
case right.right
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
⊢ IsMetaVarOrAllDefInEnv E (eq_ h1_y h1_z)
Tactic:
constructor
State after:
no goals

State before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_n : ℕ
h1_name : PredName
h1_xs h1_ys : Fin h1_n → VarName
⊢ IsMetaVarOrAllDefInEnv E (eqSubPred h1_name h1_n h1_xs h1_ys)
Tactic:
sorry
State after:
no goals

State before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ h1_Γ' : List (VarName × MetaVarName)
h1_Δ h1_Δ' : List Formula
h1_phi : Formula
h1_σ : Instantiation
h1_τ : MetaInstantiation
h1_1 : ∀ X ∈ h1_phi.metaVarSet, IsMetaVarOrAllDefInEnv E (h1_τ X)
h1_2 : ∀ (x : VarName) (X : MetaVarName), (x, X) ∈ h1_Γ → NotFree h1_Γ' (↑h1_σ x) (h1_τ X)
h1_3 : ∀ psi ∈ h1_Δ, IsProof E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)
h1_4 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih_1 : ∀ psi ∈ h1_Δ, IsMetaVarOrAllDefInEnv E (sub h1_σ h1_τ psi)
h1_ih_2 : IsMetaVarOrAllDefInEnv E h1_phi
⊢ IsMetaVarOrAllDefInEnv E (sub h1_σ h1_τ h1_phi)
Tactic:
exact lem_2_a E h1_σ h1_τ h1_phi h1_ih_2 h1_1
State after:
no goals

State before:
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_phi' : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi'
h1_2 : IsProof E h1_Γ h1_Δ h1_phi
h1_3 : IsConv E h1_phi h1_phi'
h1_ih : IsMetaVarOrAllDefInEnv E h1_phi
⊢ IsMetaVarOrAllDefInEnv E h1_phi'
Tactic:
exact h1_1
State after:
no goals