simpa using hΓ r hr₁
α : 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_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
r : Formula α
hr : r ∈ List.remove p Γ
hr₁ : r ∈ Γ
hr₂ : r ≠ p
⊢ ?m.615290
no goals