simp_all
case himp.mp.intro.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
this : (𝓓)-Consistent (insert p t.tableau.1, {q})
t' : SaturatedConsistentTableau 𝓓
right✝¹ : q ∈ t'.tableau.2
left✝ : p ∈ t'.tableau.1
right✝ : t.tableau.1 ⊆ t'.tableau.1
⊢ t.tableau.1 ⊆ t'.tableau.1 ∧ p ∈ t'.tableau.1 ∧ q ∉ t'.tableau.1
case himp.mp.intro.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
this : (𝓓)-Consistent (insert p t.tableau.1, {q})
t' : SaturatedConsistentTableau 𝓓
right✝¹ : q ∈ t'.tableau.2
left✝ : p ∈ t'.tableau.1
right✝ : t.tableau.1 ⊆ t'.tableau.1
⊢ q ∉ t'.tableau.1