Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1 : IsProof E Γ Δ F
h2 : E.WellFormed
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ Δ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E F
Tactic:
induction h1 generalizing M
Proof state after:
case hyp
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
phi✝ : Formula
a✝¹ : IsMetaVarOrAllDefInEnv E phi✝
a✝ : phi✝ ∈ Δ✝
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ✝ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ Δ✝ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E phi✝

case mp
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
phi✝ psi✝ : Formula
a✝¹ : IsProof E Γ✝ Δ✝ phi✝
a✝ : IsProof E Γ✝ Δ✝ (phi✝.imp_ psi✝)
a_ih✝¹ :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ✝ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ Δ✝ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E phi✝
a_ih✝ :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ✝ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ Δ✝ → Holds D I V M E F) →
        ∀ (V : Valuation D), Holds D I V M E (phi✝.imp_ psi✝)
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ✝ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ Δ✝ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E psi✝

case prop_1
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
phi✝ psi✝ : Formula
a✝¹ : IsMetaVarOrAllDefInEnv E phi✝
a✝ : IsMetaVarOrAllDefInEnv E psi✝
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ✝ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ Δ✝ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E (phi✝.imp_ (psi✝.imp_ phi✝))

case prop_2
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
phi✝ psi✝ chi✝ : Formula
a✝² : IsMetaVarOrAllDefInEnv E phi✝
a✝¹ : IsMetaVarOrAllDefInEnv E psi✝
a✝ : IsMetaVarOrAllDefInEnv E chi✝
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ✝ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ Δ✝ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E ((phi✝.imp_ (psi✝.imp_ chi✝)).imp_ ((phi✝.imp_ psi✝).imp_ (phi✝.imp_ chi✝)))

case prop_3
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
phi✝ psi✝ : Formula
a✝¹ : IsMetaVarOrAllDefInEnv E phi✝
a✝ : IsMetaVarOrAllDefInEnv E psi✝
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ✝ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ Δ✝ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E ((phi✝.not_.imp_ psi✝.not_).imp_ (psi✝.imp_ phi✝))

case gen
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
phi✝ : Formula
x✝ : VarName
a✝ : IsProof E Γ✝ Δ✝ phi✝
a_ih✝ :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ✝ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ Δ✝ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E phi✝
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ✝ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ Δ✝ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E (forall_ x✝ phi✝)

case pred_1
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
phi✝ psi✝ : Formula
x✝ : VarName
a✝¹ : IsMetaVarOrAllDefInEnv E phi✝
a✝ : IsMetaVarOrAllDefInEnv E psi✝
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ✝ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ Δ✝ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E ((forall_ x✝ (phi✝.imp_ psi✝)).imp_ ((forall_ x✝ phi✝).imp_ (forall_ x✝ psi✝)))

case pred_2
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
phi✝ : Formula
x✝ : VarName
a✝¹ : IsMetaVarOrAllDefInEnv E phi✝
a✝ : NotFree Γ✝ x✝ phi✝
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ✝ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ Δ✝ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E (phi✝.imp_ (forall_ x✝ phi✝))

case eq_1
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
x✝ y✝ : VarName
a✝ : ¬y✝ = x✝
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ✝ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ Δ✝ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E (exists_ x✝ (eq_ x✝ y✝))

case eq_2
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
x✝ y✝ z✝ : VarName
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ✝ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ Δ✝ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E ((eq_ x✝ y✝).imp_ ((eq_ x✝ z✝).imp_ (eq_ y✝ z✝)))

case eq_3
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
n✝ : ℕ
name✝ : PredName
xs✝ ys✝ : Fin n✝ → VarName
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ✝ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ Δ✝ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E (eqSubPred name✝ n✝ xs✝ ys✝)

case thm
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
Γ✝ Γ'✝ : 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 ∈ Δ✝,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ'✝ → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ Δ'✝ → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub σ✝ τ✝ psi)
a_ih✝ :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ✝ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ Δ✝ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E phi✝
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ'✝ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ Δ'✝ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E (sub σ✝ τ✝ phi✝)

case conv
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
Γ✝ : List (VarName × MetaVarName)
Δ✝ : List Formula
phi✝ phi'✝ : Formula
a✝² : IsMetaVarOrAllDefInEnv E phi'✝
a✝¹ : IsProof E Γ✝ Δ✝ phi✝
a✝ : IsConv E phi✝ phi'✝
a_ih✝ :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ✝ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ Δ✝ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E phi✝
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ Γ✝ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ Δ✝ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E phi'✝