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 : IsProof E Γ Δ F
⊢ IsMetaVarOrAllDefInEnv E F
Tactic:
induction h1
Proof 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'✝