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

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
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'✝

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : h1_phi ∈ h1_Δ
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
⊢ ∀ (V : Valuation D), Holds D I V M E h1_phi
Tactic:
case hyp h1_Γ h1_Δ h1_phi h1_1 h1_2 =>
  intro V
  exact hyp h1_phi V h1_2
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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 :
  ∀ (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
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.imp_ h1_psi)
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
⊢ ∀ (V : Valuation D), Holds D I V M E h1_psi
Tactic:
case mp h1_Γ h1_Δ h1_phi h1_psi h1_1 h1_2 h1_ih_1 h1_ih_2 =>
  simp only [Holds] at h1_ih_2
  intro V
  exact h1_ih_2 M nf hyp V (h1_ih_1 M nf hyp V)
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (h1_psi.imp_ h1_phi))
Tactic:
case prop_1 h1_Γ h1_Δ h1_phi h1_psi h1_1 h1_2 =>
  simp only [Holds]
  intro V a1 a2
  exact a1
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
⊢ ∀ (V : Valuation D),
    Holds D I V M 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 =>
  simp only [Holds]
  intro V a1 a2 a3
  apply a1 a3
  exact a2 a3
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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
⊢ ∀ (V : Valuation D), Holds D I V M 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 =>
  simp only [Holds]
  intro V a1 a2
  by_contra contra
  exact a1 contra a2
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi : Formula
h1_x : VarName
h1_1 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih :
  ∀ (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
⊢ ∀ (V : Valuation D), Holds D I V M E (forall_ h1_x h1_phi)
Tactic:
case gen h1_Γ h1_Δ h1_phi h1_x h1_1 h1_ih =>
  simp only [Holds]
  intro V d
  exact h1_ih M nf hyp (Function.updateITE V h1_x d)
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
⊢ ∀ (V : Valuation D),
    Holds D I V M 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 =>
  simp only [Holds]
  intro V a1 a2 d
  apply a1 d
  exact a2 d
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (forall_ h1_x h1_phi))
Tactic:
case pred_2 h1_Γ h1_Δ h1_phi h1_x h1_1 h1_2 =>
  have s1 : IsNotFree D I M E h1_phi h1_x
  apply not_free_imp_is_not_free D I M E h1_phi h1_Γ h1_x h1_2
  exact nf h1_x
  simp only [Holds]
  intro V a1 a
  unfold IsNotFree at s1
  simp only [← s1 V a]
  exact a1
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
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
⊢ ∀ (V : Valuation D), Holds D I V M E (exists_ h1_x (eq_ h1_x h1_y))
Tactic:
case eq_1 h1_Γ h1_Δ h1_x h1_y h1_1 =>
  unfold exists_
  simp only [Holds]
  simp
  intro V
  apply Exists.intro (V h1_y)
  unfold Function.updateITE
  simp
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_n : ℕ
h1_name : PredName
h1_xs h1_ys : Fin h1_n → VarName
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
⊢ ∀ (V : Valuation D), Holds D I V M 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:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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 :
  ∀ (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
⊢ ∀ (V : Valuation D), Holds D I V M E h1_phi'
Tactic:
case conv h1_Γ h1_Δ h1_phi h1_phi' h1_1 h1_2 h1_3 h1_ih =>
  intro V
  have s1 : Holds D I V M E h1_phi := h1_ih M nf hyp V
  simp only [← holds_conv D I V M E h1_phi h1_phi' h2 h1_3]
  exact s1
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : h1_phi ∈ h1_Δ
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
⊢ ∀ (V : Valuation D), Holds D I V M E h1_phi
Tactic:
intro V
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : h1_phi ∈ h1_Δ
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
V : Valuation D
⊢ Holds D I V M E h1_phi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : h1_phi ∈ h1_Δ
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
V : Valuation D
⊢ Holds D I V M E h1_phi
Tactic:
exact hyp h1_phi V h1_2
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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 :
  ∀ (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
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.imp_ h1_psi)
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
⊢ ∀ (V : Valuation D), Holds D I V M E h1_psi
Tactic:
simp only [Holds] at h1_ih_2
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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 :
  ∀ (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
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 → Holds D I V M E h1_psi
⊢ ∀ (V : Valuation D), Holds D I V M E h1_psi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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 :
  ∀ (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
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 → Holds D I V M E h1_psi
⊢ ∀ (V : Valuation D), Holds D I V M E h1_psi
Tactic:
intro V
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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 :
  ∀ (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
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 → Holds D I V M E h1_psi
V : Valuation D
⊢ Holds D I V M E h1_psi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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 :
  ∀ (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
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 → Holds D I V M E h1_psi
V : Valuation D
⊢ Holds D I V M E h1_psi
Tactic:
exact h1_ih_2 M nf hyp V (h1_ih_1 M nf hyp V)
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (h1_psi.imp_ h1_phi))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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
⊢ ∀ (V : Valuation D), Holds D I V M E h1_phi → Holds D I V M E h1_psi → Holds D I V M E h1_phi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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
⊢ ∀ (V : Valuation D), Holds D I V M E h1_phi → Holds D I V M E h1_psi → Holds D I V M E h1_phi
Tactic:
intro V a1 a2
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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
V : Valuation D
a1 : Holds D I V M E h1_phi
a2 : Holds D I V M E h1_psi
⊢ Holds D I V M E h1_phi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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
V : Valuation D
a1 : Holds D I V M E h1_phi
a2 : Holds D I V M E h1_psi
⊢ Holds D I V M E h1_phi
Tactic:
exact a1
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
⊢ ∀ (V : Valuation D),
    Holds D I V M E ((h1_phi.imp_ (h1_psi.imp_ h1_chi)).imp_ ((h1_phi.imp_ h1_psi).imp_ (h1_phi.imp_ h1_chi)))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
⊢ ∀ (V : Valuation D),
    (Holds D I V M E h1_phi → Holds D I V M E h1_psi → Holds D I V M E h1_chi) →
      (Holds D I V M E h1_phi → Holds D I V M E h1_psi) → Holds D I V M E h1_phi → Holds D I V M E h1_chi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
⊢ ∀ (V : Valuation D),
    (Holds D I V M E h1_phi → Holds D I V M E h1_psi → Holds D I V M E h1_chi) →
      (Holds D I V M E h1_phi → Holds D I V M E h1_psi) → Holds D I V M E h1_phi → Holds D I V M E h1_chi
Tactic:
intro V a1 a2 a3
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
V : Valuation D
a1 : Holds D I V M E h1_phi → Holds D I V M E h1_psi → Holds D I V M E h1_chi
a2 : Holds D I V M E h1_phi → Holds D I V M E h1_psi
a3 : Holds D I V M E h1_phi
⊢ Holds D I V M E h1_chi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
V : Valuation D
a1 : Holds D I V M E h1_phi → Holds D I V M E h1_psi → Holds D I V M E h1_chi
a2 : Holds D I V M E h1_phi → Holds D I V M E h1_psi
a3 : Holds D I V M E h1_phi
⊢ Holds D I V M E h1_chi
Tactic:
apply a1 a3
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
V : Valuation D
a1 : Holds D I V M E h1_phi → Holds D I V M E h1_psi → Holds D I V M E h1_chi
a2 : Holds D I V M E h1_phi → Holds D I V M E h1_psi
a3 : Holds D I V M E h1_phi
⊢ Holds D I V M E h1_psi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
V : Valuation D
a1 : Holds D I V M E h1_phi → Holds D I V M E h1_psi → Holds D I V M E h1_chi
a2 : Holds D I V M E h1_phi → Holds D I V M E h1_psi
a3 : Holds D I V M E h1_phi
⊢ Holds D I V M E h1_psi
Tactic:
exact a2 a3
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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
⊢ ∀ (V : Valuation D), Holds D I V M E ((h1_phi.not_.imp_ h1_psi.not_).imp_ (h1_psi.imp_ h1_phi))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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
⊢ ∀ (V : Valuation D),
    (¬Holds D I V M E h1_phi → ¬Holds D I V M E h1_psi) → Holds D I V M E h1_psi → Holds D I V M E h1_phi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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
⊢ ∀ (V : Valuation D),
    (¬Holds D I V M E h1_phi → ¬Holds D I V M E h1_psi) → Holds D I V M E h1_psi → Holds D I V M E h1_phi
Tactic:
intro V a1 a2
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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
V : Valuation D
a1 : ¬Holds D I V M E h1_phi → ¬Holds D I V M E h1_psi
a2 : Holds D I V M E h1_psi
⊢ Holds D I V M E h1_phi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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
V : Valuation D
a1 : ¬Holds D I V M E h1_phi → ¬Holds D I V M E h1_psi
a2 : Holds D I V M E h1_psi
⊢ Holds D I V M E h1_phi
Tactic:
by_contra contra
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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
V : Valuation D
a1 : ¬Holds D I V M E h1_phi → ¬Holds D I V M E h1_psi
a2 : Holds D I V M E h1_psi
contra : ¬Holds D I V M E h1_phi
⊢ False

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
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
V : Valuation D
a1 : ¬Holds D I V M E h1_phi → ¬Holds D I V M E h1_psi
a2 : Holds D I V M E h1_psi
contra : ¬Holds D I V M E h1_phi
⊢ False
Tactic:
exact a1 contra a2
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi : Formula
h1_x : VarName
h1_1 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih :
  ∀ (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
⊢ ∀ (V : Valuation D), Holds D I V M E (forall_ h1_x h1_phi)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi : Formula
h1_x : VarName
h1_1 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih :
  ∀ (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
⊢ ∀ (V : Valuation D) (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi : Formula
h1_x : VarName
h1_1 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih :
  ∀ (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
⊢ ∀ (V : Valuation D) (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi
Tactic:
intro V d
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi : Formula
h1_x : VarName
h1_1 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih :
  ∀ (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
V : Valuation D
d : D
⊢ Holds D I (Function.updateITE V h1_x d) M E h1_phi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi : Formula
h1_x : VarName
h1_1 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih :
  ∀ (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
V : Valuation D
d : D
⊢ Holds D I (Function.updateITE V h1_x d) M E h1_phi
Tactic:
exact h1_ih M nf hyp (Function.updateITE V h1_x d)
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
⊢ ∀ (V : Valuation D),
    Holds D I V M E ((forall_ h1_x (h1_phi.imp_ h1_psi)).imp_ ((forall_ h1_x h1_phi).imp_ (forall_ h1_x h1_psi)))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
⊢ ∀ (V : Valuation D),
    (∀ (d : D),
        Holds D I (Function.updateITE V h1_x d) M E h1_phi → Holds D I (Function.updateITE V h1_x d) M E h1_psi) →
      (∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi) →
        ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_psi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
⊢ ∀ (V : Valuation D),
    (∀ (d : D),
        Holds D I (Function.updateITE V h1_x d) M E h1_phi → Holds D I (Function.updateITE V h1_x d) M E h1_psi) →
      (∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi) →
        ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_psi
Tactic:
intro V a1 a2 d
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
V : Valuation D
a1 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi → Holds D I (Function.updateITE V h1_x d) M E h1_psi
a2 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi
d : D
⊢ Holds D I (Function.updateITE V h1_x d) M E h1_psi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
V : Valuation D
a1 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi → Holds D I (Function.updateITE V h1_x d) M E h1_psi
a2 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi
d : D
⊢ Holds D I (Function.updateITE V h1_x d) M E h1_psi
Tactic:
apply a1 d
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
V : Valuation D
a1 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi → Holds D I (Function.updateITE V h1_x d) M E h1_psi
a2 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi
d : D
⊢ Holds D I (Function.updateITE V h1_x d) M E h1_phi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
V : Valuation D
a1 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi → Holds D I (Function.updateITE V h1_x d) M E h1_psi
a2 : ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi
d : D
⊢ Holds D I (Function.updateITE V h1_x d) M E h1_phi
Tactic:
exact a2 d
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (forall_ h1_x h1_phi))
Tactic:
have s1 : IsNotFree D I M E h1_phi h1_x
State after:
case s1
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
⊢ IsNotFree D I M E h1_phi h1_x

D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
s1 : IsNotFree D I M E h1_phi h1_x
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (forall_ h1_x h1_phi))

State before:
case s1
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
⊢ IsNotFree D I M E h1_phi h1_x

D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
s1 : IsNotFree D I M E h1_phi h1_x
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (forall_ h1_x h1_phi))
Tactic:
apply not_free_imp_is_not_free D I M E h1_phi h1_Γ h1_x h1_2
State after:
case s1
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
⊢ ∀ (X : MetaVarName), (h1_x, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) h1_x

D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
s1 : IsNotFree D I M E h1_phi h1_x
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (forall_ h1_x h1_phi))

State before:
case s1
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
⊢ ∀ (X : MetaVarName), (h1_x, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) h1_x

D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
s1 : IsNotFree D I M E h1_phi h1_x
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (forall_ h1_x h1_phi))
Tactic:
exact nf h1_x
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
s1 : IsNotFree D I M E h1_phi h1_x
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (forall_ h1_x h1_phi))

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
s1 : IsNotFree D I M E h1_phi h1_x
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (forall_ h1_x h1_phi))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
s1 : IsNotFree D I M E h1_phi h1_x
⊢ ∀ (V : Valuation D), Holds D I V M E h1_phi → ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
s1 : IsNotFree D I M E h1_phi h1_x
⊢ ∀ (V : Valuation D), Holds D I V M E h1_phi → ∀ (d : D), Holds D I (Function.updateITE V h1_x d) M E h1_phi
Tactic:
intro V a1 a
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
s1 : IsNotFree D I M E h1_phi h1_x
V : Valuation D
a1 : Holds D I V M E h1_phi
a : D
⊢ Holds D I (Function.updateITE V h1_x a) M E h1_phi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
s1 : IsNotFree D I M E h1_phi h1_x
V : Valuation D
a1 : Holds D I V M E h1_phi
a : D
⊢ Holds D I (Function.updateITE V h1_x a) M E h1_phi
Tactic:
unfold IsNotFree at s1
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
s1 : ∀ (V : Valuation D) (d : D), Holds D I V M E h1_phi ↔ Holds D I (Function.updateITE V h1_x d) M E h1_phi
V : Valuation D
a1 : Holds D I V M E h1_phi
a : D
⊢ Holds D I (Function.updateITE V h1_x a) M E h1_phi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
s1 : ∀ (V : Valuation D) (d : D), Holds D I V M E h1_phi ↔ Holds D I (Function.updateITE V h1_x d) M E h1_phi
V : Valuation D
a1 : Holds D I V M E h1_phi
a : D
⊢ Holds D I (Function.updateITE V h1_x a) M E h1_phi
Tactic:
simp only [← s1 V a]
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
s1 : ∀ (V : Valuation D) (d : D), Holds D I V M E h1_phi ↔ Holds D I (Function.updateITE V h1_x d) M E h1_phi
V : Valuation D
a1 : Holds D I V M E h1_phi
a : D
⊢ Holds D I V M E h1_phi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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
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
s1 : ∀ (V : Valuation D) (d : D), Holds D I V M E h1_phi ↔ Holds D I (Function.updateITE V h1_x d) M E h1_phi
V : Valuation D
a1 : Holds D I V M E h1_phi
a : D
⊢ Holds D I V M E h1_phi
Tactic:
exact a1
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
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
⊢ ∀ (V : Valuation D), Holds D I V M E (exists_ h1_x (eq_ h1_x h1_y))
Tactic:
unfold exists_
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
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
⊢ ∀ (V : Valuation D), Holds D I V M E (forall_ h1_x (eq_ h1_x h1_y).not_).not_

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
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
⊢ ∀ (V : Valuation D), Holds D I V M E (forall_ h1_x (eq_ h1_x h1_y).not_).not_
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
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
⊢ ∀ (V : Valuation D), ¬∀ (d : D), ¬Function.updateITE V h1_x d h1_x = Function.updateITE V h1_x d h1_y

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
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
⊢ ∀ (V : Valuation D), ¬∀ (d : D), ¬Function.updateITE V h1_x d h1_x = Function.updateITE V h1_x d h1_y
Tactic:
simp
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
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
⊢ ∀ (V : Valuation D), ∃ x, Function.updateITE V h1_x x h1_x = Function.updateITE V h1_x x h1_y

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
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
⊢ ∀ (V : Valuation D), ∃ x, Function.updateITE V h1_x x h1_x = Function.updateITE V h1_x x h1_y
Tactic:
intro V
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
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
V : Valuation D
⊢ ∃ x, Function.updateITE V h1_x x h1_x = Function.updateITE V h1_x x h1_y

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
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
V : Valuation D
⊢ ∃ x, Function.updateITE V h1_x x h1_x = Function.updateITE V h1_x x h1_y
Tactic:
apply Exists.intro (V h1_y)
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
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
V : Valuation D
⊢ Function.updateITE V h1_x (V h1_y) h1_x = Function.updateITE V h1_x (V h1_y) h1_y

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
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
V : Valuation D
⊢ Function.updateITE V h1_x (V h1_y) h1_x = Function.updateITE V h1_x (V h1_y) h1_y
Tactic:
unfold Function.updateITE
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
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
V : Valuation D
⊢ (if h1_x = h1_x then V h1_y else V h1_x) = if h1_y = h1_x then V h1_y else V h1_y

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
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
V : Valuation D
⊢ (if h1_x = h1_x then V h1_y else V h1_x) = if h1_y = h1_x then V h1_y else V h1_y
Tactic:
simp
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
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
⊢ ∀ (V : Valuation D), Holds D I V M E ((eq_ h1_x h1_y).imp_ ((eq_ h1_x h1_z).imp_ (eq_ h1_y h1_z)))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
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
⊢ ∀ (V : Valuation D), V h1_x = V h1_y → V h1_x = V h1_z → V h1_y = V h1_z

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
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
⊢ ∀ (V : Valuation D), V h1_x = V h1_y → V h1_x = V h1_z → V h1_y = V h1_z
Tactic:
intro V a1 a2
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
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
V : Valuation D
a1 : V h1_x = V h1_y
a2 : V h1_x = V h1_z
⊢ V h1_y = V h1_z

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
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
V : Valuation D
a1 : V h1_x = V h1_y
a2 : V h1_x = V h1_z
⊢ V h1_y = V h1_z
Tactic:
trans V h1_x
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
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
V : Valuation D
a1 : V h1_x = V h1_y
a2 : V h1_x = V h1_z
⊢ V h1_y = V h1_x

D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
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
V : Valuation D
a1 : V h1_x = V h1_y
a2 : V h1_x = V h1_z
⊢ V h1_x = V h1_z

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
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
V : Valuation D
a1 : V h1_x = V h1_y
a2 : V h1_x = V h1_z
⊢ V h1_y = V h1_x
Tactic:
simp only [a1]
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
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
V : Valuation D
a1 : V h1_x = V h1_y
a2 : V h1_x = V h1_z
⊢ V h1_x = V h1_z
Tactic:
exact a2
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_n : ℕ
h1_name : PredName
h1_xs h1_ys : Fin h1_n → VarName
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
⊢ ∀ (V : Valuation D), Holds D I V M E (eqSubPred h1_name h1_n h1_xs h1_ys)
Tactic:
sorry
State after:
no goals

State before:
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
⊢ ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ h1_phi)
Tactic:
obtain ⟨σ', a1⟩ := h1_σ.2
State after:
case intro
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
⊢ ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ h1_phi)

State before:
case intro
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
⊢ ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ h1_phi)
Tactic:
have s1 : IsMetaVarOrAllDefInEnv E h1_phi := is_proof_imp_is_meta_var_or_all_def_in_env E h1_Γ h1_Δ h1_phi h1_4
State after:
case intro
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), Holds D I V M E (sub h1_σ h1_τ h1_phi)

State before:
case intro
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), Holds D I V M E (sub h1_σ h1_τ h1_phi)
Tactic:
intro V
State after:
case intro
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
⊢ Holds D I V M E (sub h1_σ h1_τ h1_phi)

State before:
case intro
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
⊢ Holds D I V M E (sub h1_σ h1_τ h1_phi)
Tactic:
simp only [← holds_sub D I V M E h1_σ σ' h1_τ h1_phi s1 a1]
State after:
case intro
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
⊢ Holds D I (V ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E h1_phi

State before:
case intro
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
⊢ Holds D I (V ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E h1_phi
Tactic:
apply h1_ih_2
State after:
case intro.nf
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
⊢ ∀ (v : VarName) (X : MetaVarName),
    (v, X) ∈ h1_Γ → IsNotFree D I (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E (meta_var_ X) v

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
⊢ ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E F

State before:
case intro.nf
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
⊢ ∀ (v : VarName) (X : MetaVarName),
    (v, X) ∈ h1_Γ → IsNotFree D I (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E (meta_var_ X) v
Tactic:
intro v X a2
State after:
case intro.nf
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
v : VarName
X : MetaVarName
a2 : (v, X) ∈ h1_Γ
⊢ IsNotFree D I (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E (meta_var_ X) v

State before:
case intro.nf
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
v : VarName
X : MetaVarName
a2 : (v, X) ∈ h1_Γ
⊢ IsNotFree D I (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E (meta_var_ X) v
Tactic:
exact lem_1 D I M E h1_Γ h1_Γ' h1_σ σ' h1_τ a1 nf h1_2 v X a2
State after:
no goals

State before:
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
⊢ ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E F
Tactic:
intro psi V' a2
State after:
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_Δ
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi

State before:
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_Δ
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
Tactic:
have s2 : IsMetaVarOrAllDefInEnv E psi
State after:
case s2
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 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

State before:
case s2
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 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 lem_2_b E h1_σ h1_τ
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_Δ
⊢ 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

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)
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

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_Δ
⊢ 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
Tactic:
exact h1_3 psi a2
State after:
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

State before:
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:
have s3 : ∀ V'' : Valuation D, Holds D I (V'' ∘ h1_σ.val) (fun (X' : MetaVarName) (V' : Valuation D) => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
State after:
case s3
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
⊢ ∀ (V'' : Valuation D), Holds D I (V'' ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E 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
s3 : ∀ (V'' : Valuation D), Holds D I (V'' ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi

State before:
case s3
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
⊢ ∀ (V'' : Valuation D), Holds D I (V'' ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E 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
s3 : ∀ (V'' : Valuation D), Holds D I (V'' ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
Tactic:
intro V''
State after:
case s3
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
V'' : Valuation D
⊢ Holds D I (V'' ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E 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
s3 : ∀ (V'' : Valuation D), Holds D I (V'' ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi

State before:
case s3
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
V'' : Valuation D
⊢ Holds D I (V'' ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E 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
s3 : ∀ (V'' : Valuation D), Holds D I (V'' ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
Tactic:
simp only [holds_sub D I V'' M E h1_σ σ' h1_τ psi s2 a1]
State after:
case s3
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
V'' : Valuation D
⊢ Holds D I V'' M 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
s3 : ∀ (V'' : Valuation D), Holds D I (V'' ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi

State before:
case s3
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
V'' : Valuation D
⊢ Holds D I V'' M 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
s3 : ∀ (V'' : Valuation D), Holds D I (V'' ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
Tactic:
exact h1_ih_1 psi a2 M nf hyp V''
State after:
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
s3 : ∀ (V'' : Valuation D), Holds D I (V'' ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi

State before:
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
s3 : ∀ (V'' : Valuation D), Holds D I (V'' ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
Tactic:
specialize s3 (V' ∘ σ')
State after:
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
s3 : Holds D I ((V' ∘ σ') ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi

State before:
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
s3 : Holds D I ((V' ∘ σ') ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
Tactic:
simp only [Function.comp.assoc] at s3
State after:
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
s3 : Holds D I (V' ∘ σ' ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi

State before:
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
s3 : Holds D I (V' ∘ σ' ∘ ↑h1_σ) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
Tactic:
simp only [a1.right] at s3
State after:
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
s3 : Holds D I (V' ∘ id) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi

State before:
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
s3 : Holds D I (V' ∘ id) (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
Tactic:
simp only [Function.comp_id] at s3
State after:
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
s3 : Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi

State before:
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
s3 : Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
Tactic:
exact s3
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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 :
  ∀ (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
⊢ ∀ (V : Valuation D), Holds D I V M E h1_phi'
Tactic:
intro V
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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 :
  ∀ (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
V : Valuation D
⊢ Holds D I V M E h1_phi'

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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 :
  ∀ (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
V : Valuation D
⊢ Holds D I V M E h1_phi'
Tactic:
have s1 : Holds D I V M E h1_phi := h1_ih M nf hyp V
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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 :
  ∀ (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
V : Valuation D
s1 : Holds D I V M E h1_phi
⊢ Holds D I V M E h1_phi'

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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 :
  ∀ (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
V : Valuation D
s1 : Holds D I V M E h1_phi
⊢ Holds D I V M E h1_phi'
Tactic:
simp only [← holds_conv D I V M E h1_phi h1_phi' h2 h1_3]
State after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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 :
  ∀ (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
V : Valuation D
s1 : Holds D I V M E h1_phi
⊢ Holds D I V M E h1_phi

State before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
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 :
  ∀ (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
V : Valuation D
s1 : Holds D I V M E h1_phi
⊢ Holds D I V M E h1_phi
Tactic:
exact s1
State after:
no goals