Theorem: MM0.holds_is_proof
Proof state before:
case s2.h1
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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_Δ,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ psi)
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F
σ' : VarName → VarName
a1 : ↑h1_σ ∘ σ' = id ∧ σ' ∘ ↑h1_σ = id
s1 : IsMetaVarOrAllDefInEnv E h1_phi
V : Valuation D
psi : Formula
V' : Valuation D
a2 : psi ∈ h1_Δ
⊢ IsMetaVarOrAllDefInEnv E (sub h1_σ h1_τ psi)

case intro.hyp
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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_Δ,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ psi)
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F
σ' : VarName → VarName
a1 : ↑h1_σ ∘ σ' = id ∧ σ' ∘ ↑h1_σ = id
s1 : IsMetaVarOrAllDefInEnv E h1_phi
V : Valuation D
psi : Formula
V' : Valuation D
a2 : psi ∈ h1_Δ
s2 : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
Tactic:
apply is_proof_imp_is_meta_var_or_all_def_in_env E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)
Proof state after:
case s2.h1
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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_Δ,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ psi)
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F
σ' : VarName → VarName
a1 : ↑h1_σ ∘ σ' = id ∧ σ' ∘ ↑h1_σ = id
s1 : IsMetaVarOrAllDefInEnv E h1_phi
V : Valuation D
psi : Formula
V' : Valuation D
a2 : psi ∈ h1_Δ
⊢ IsProof E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)

case intro.hyp
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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_Δ,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ psi)
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F
σ' : VarName → VarName
a1 : ↑h1_σ ∘ σ' = id ∧ σ' ∘ ↑h1_σ = id
s1 : IsMetaVarOrAllDefInEnv E h1_phi
V : Valuation D
psi : Formula
V' : Valuation D
a2 : psi ∈ h1_Δ
s2 : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi