internlm/Lean-Github huggingface dataset:
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_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
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_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
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_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
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_Γ 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
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_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
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:
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:
unfold IsMetaVarOrAllDefInEnv at h1_ih_2
Proof 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
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 ∧ IsMetaVarOrAllDefInEnv E h1_psi
⊢ IsMetaVarOrAllDefInEnv E h1_psi
Tactic:
cases h1_ih_2
Proof 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
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 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
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 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
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:
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:
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
Proof state after:
no goals
Theorem: MM0.is_proof_imp_is_meta_var_or_all_def_in_env
Proof 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
Proof 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
Theorem: MM0.is_proof_imp_is_meta_var_or_all_def_in_env
Proof 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
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:
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:
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
Proof state after:
no goals
Theorem: MM0.is_proof_imp_is_meta_var_or_all_def_in_env
Proof 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
Proof 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
Theorem: MM0.is_proof_imp_is_meta_var_or_all_def_in_env
Proof 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
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:
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:
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:
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:
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:
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:
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
Proof state after:
no goals
Theorem: MM0.is_proof_imp_is_meta_var_or_all_def_in_env
Proof 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
Proof 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)
Theorem: MM0.is_proof_imp_is_meta_var_or_all_def_in_env
Proof 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
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:
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:
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
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:
constructor
Proof 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)
Theorem: MM0.is_proof_imp_is_meta_var_or_all_def_in_env
Proof 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
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_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
⊢ IsMetaVarOrAllDefInEnv E (exists_ h1_x (eq_ h1_x h1_y))
Tactic:
unfold exists_
Proof 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_
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_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
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_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
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_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
⊢ IsMetaVarOrAllDefInEnv E (forall_ h1_x (eq_ h1_x h1_y).not_).not_
Tactic:
constructor
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_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
Proof 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))
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_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
Proof state after:
no goals
Theorem: MM0.is_proof_imp_is_meta_var_or_all_def_in_env
Proof 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
Proof state after:
no goals
Theorem: MM0.is_proof_imp_is_meta_var_or_all_def_in_env
Proof 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
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_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
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_Γ 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
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_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
Proof state after:
no goals
Theorem: MM0.lem_4
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
E : Env
d : Definition
name : DefName
args : List VarName
h1 : E.WellFormed
h2 : d ∈ E
h3 : name = d.name ∧ args.length = d.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M E d.F ↔ Holds D I V M E (def_ name args)
Tactic:
induction E
Proof state after:
case nil
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
h1 : Env.WellFormed []
h2 : d ∈ []
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M [] d.F ↔ Holds D I V M [] (def_ name args)

case cons
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  Env.WellFormed tail✝ →
    d ∈ tail✝ →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tail✝ d.F ↔ Holds D I V M tail✝ (def_ name args))
h1 : Env.WellFormed (head✝ :: tail✝)
h2 : d ∈ head✝ :: tail✝
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (head✝ :: tail✝) d.F ↔
    Holds D I V M (head✝ :: tail✝) (def_ name args)
Theorem: MM0.lem_4
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
h1 : Env.WellFormed []
h2 : d ∈ []
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M [] d.F ↔ Holds D I V M [] (def_ name args)
Tactic:
case nil =>
  simp at h2
Proof state after:
no goals
Theorem: MM0.lem_4
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
h1 : Env.WellFormed []
h2 : d ∈ []
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M [] d.F ↔ Holds D I V M [] (def_ name args)
Tactic:
simp at h2
Proof state after:
no goals