have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! Δ.disj' := (by_axm! (by simp)) ⨀ this
case h.h
α : 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
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p
⊢ [p, p ⟶ Δ.disj'] ⊢[𝓓]! q
case h.h
α : 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
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this✝ : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p
this : [p, p ⟶ Δ.disj'] ⊢[𝓓]! Δ.disj'
⊢ [p, p ⟶ Δ.disj'] ⊢[𝓓]! q