Theorem: LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel (Logic/Propositional/Superintuitionistic/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ CanonicalModel 𝓓 ⊧ p ↔ 𝓓 ⊢! p
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ CanonicalModel 𝓓 ⊧ p → 𝓓 ⊢! p

case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ 𝓓 ⊢! p → CanonicalModel 𝓓 ⊧ p

State before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ CanonicalModel 𝓓 ⊧ p → 𝓓 ⊢! p

case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ 𝓓 ⊢! p → CanonicalModel 𝓓 ⊧ p
Tactic:
. contrapose;
  intro h;
  have : (𝓓)-Consistent (∅, {p}) := by
    simp only [Tableau.ParametricConsistent, Collection.not_mem_empty, imp_false, Set.mem_singleton_iff];
    rintro Γ Δ hΓ hΔ;
    by_contra hC;
    replace hΓ : Γ = [] := List.nil_iff.mpr hΓ;
    subst hΓ;
    have : 𝓓 ⊢! p := disj_allsame'! hΔ (hC ⨀ verum!);
    contradiction;
  obtain ⟨t', ht'⟩ := lindenbaum this;
  simp [ValidOnModel.iff_models, ValidOnModel]
  existsi t';
  apply truthlemma.not.mpr;
  apply t'.not_mem₁_iff_mem₂.mpr;
  simp_all;
State after:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ 𝓓 ⊢! p → CanonicalModel 𝓓 ⊧ p

State before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ 𝓓 ⊢! p → CanonicalModel 𝓓 ⊧ p
Tactic:
. intro h t;
  suffices p ∈ t.tableau.1 by exact truthlemma.mpr this;
  exact mem₁_of_provable h;
State after:
no goals

State before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ CanonicalModel 𝓓 ⊧ p → 𝓓 ⊢! p
Tactic:
contrapose
State after:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ ¬𝓓 ⊢! p → ¬CanonicalModel 𝓓 ⊧ p

State before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ ¬𝓓 ⊢! p → ¬CanonicalModel 𝓓 ⊧ p
Tactic:
intro h
State after:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
⊢ ¬CanonicalModel 𝓓 ⊧ p

State before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
⊢ ¬CanonicalModel 𝓓 ⊧ p
Tactic:
have : (𝓓)-Consistent (∅, {p}) := by
  simp only [Tableau.ParametricConsistent, Collection.not_mem_empty, imp_false, Set.mem_singleton_iff];
  rintro Γ Δ hΓ hΔ;
  by_contra hC;
  replace hΓ : Γ = [] := List.nil_iff.mpr hΓ;
  subst hΓ;
  have : 𝓓 ⊢! p := disj_allsame'! hΔ (hC ⨀ verum!);
  contradiction;
State after:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
⊢ ¬CanonicalModel 𝓓 ⊧ p

State before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
⊢ ¬CanonicalModel 𝓓 ⊧ p
Tactic:
obtain ⟨t', ht'⟩ := lindenbaum this
State after:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ ¬CanonicalModel 𝓓 ⊧ p

State before:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ ¬CanonicalModel 𝓓 ⊧ p
Tactic:
simp [ValidOnModel.iff_models, ValidOnModel]
State after:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ ∃ x, ¬Satisfies (CanonicalModel 𝓓) x p

State before:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ ∃ x, ¬Satisfies (CanonicalModel 𝓓) x p
Tactic:
existsi t'
State after:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ ¬Satisfies (CanonicalModel 𝓓) t' p

State before:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ ¬Satisfies (CanonicalModel 𝓓) t' p
Tactic:
apply truthlemma.not.mpr
State after:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ p ∉ t'.tableau.1

State before:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ p ∉ t'.tableau.1
Tactic:
apply t'.not_mem₁_iff_mem₂.mpr
State after:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ p ∈ t'.tableau.2

State before:
case mp.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
this : (𝓓)-Consistent (∅, {p})
t' : SaturatedConsistentTableau 𝓓
ht' : (∅, {p}) ⊆ t'.tableau
⊢ p ∈ t'.tableau.2
Tactic:
simp_all
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
⊢ (𝓓)-Consistent (∅, {p})
Tactic:
simp only [Tableau.ParametricConsistent, Collection.not_mem_empty, imp_false, Set.mem_singleton_iff]
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
⊢ ∀ {Γ Δ : List (Formula α)}, (∀ (p : Formula α), p ∉ Γ) → (∀ p_1 ∈ Δ, p_1 = p) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
⊢ ∀ {Γ Δ : List (Formula α)}, (∀ (p : Formula α), p ∉ Γ) → (∀ p_1 ∈ Δ, p_1 = p) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
rintro Γ Δ hΓ hΔ
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Γ Δ : List (Formula α)
hΓ : ∀ (p : Formula α), p ∉ Γ
hΔ : ∀ p_1 ∈ Δ, p_1 = p
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Γ Δ : List (Formula α)
hΓ : ∀ (p : Formula α), p ∉ Γ
hΔ : ∀ p_1 ∈ Δ, p_1 = p
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
by_contra hC
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Γ Δ : List (Formula α)
hΓ : ∀ (p : Formula α), p ∉ Γ
hΔ : ∀ p_1 ∈ Δ, p_1 = p
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ False

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Γ Δ : List (Formula α)
hΓ : ∀ (p : Formula α), p ∉ Γ
hΔ : ∀ p_1 ∈ Δ, p_1 = p
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ False
Tactic:
replace hΓ : Γ = [] := List.nil_iff.mpr hΓ
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Γ Δ : List (Formula α)
hΔ : ∀ p_1 ∈ Δ, p_1 = p
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
hΓ : Γ = []
⊢ False

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Γ Δ : List (Formula α)
hΔ : ∀ p_1 ∈ Δ, p_1 = p
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
hΓ : Γ = []
⊢ False
Tactic:
subst hΓ
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Δ : List (Formula α)
hΔ : ∀ p_1 ∈ Δ, p_1 = p
hC : 𝓓 ⊢! [].conj' ⟶ Δ.disj'
⊢ False

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Δ : List (Formula α)
hΔ : ∀ p_1 ∈ Δ, p_1 = p
hC : 𝓓 ⊢! [].conj' ⟶ Δ.disj'
⊢ False
Tactic:
have : 𝓓 ⊢! p := disj_allsame'! hΔ (hC ⨀ verum!)
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Δ : List (Formula α)
hΔ : ∀ p_1 ∈ Δ, p_1 = p
hC : 𝓓 ⊢! [].conj' ⟶ Δ.disj'
this : 𝓓 ⊢! p
⊢ False

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
h : ¬𝓓 ⊢! p
Δ : List (Formula α)
hΔ : ∀ p_1 ∈ Δ, p_1 = p
hC : 𝓓 ⊢! [].conj' ⟶ Δ.disj'
this : 𝓓 ⊢! p
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ 𝓓 ⊢! p → CanonicalModel 𝓓 ⊧ p
Tactic:
intro h t
State after:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p : Formula α
h : 𝓓 ⊢! p
t : (CanonicalModel 𝓓).World
⊢ t ⊧ p

State before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p : Formula α
h : 𝓓 ⊢! p
t : (CanonicalModel 𝓓).World
⊢ t ⊧ p
Tactic:
suffices p ∈ t.tableau.1 by exact truthlemma.mpr this;
State after:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p : Formula α
h : 𝓓 ⊢! p
t : (CanonicalModel 𝓓).World
⊢ p ∈ t.tableau.1

State before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p : Formula α
h : 𝓓 ⊢! p
t : (CanonicalModel 𝓓).World
⊢ p ∈ t.tableau.1
Tactic:
exact mem₁_of_provable h
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p : Formula α
h : 𝓓 ⊢! p
t : (CanonicalModel 𝓓).World
this : p ∈ t.tableau.1
⊢ t ⊧ p
Tactic:
exact truthlemma.mpr this
State after:
no goals