simp [Satisfies.iff_models, Satisfies, *]
case hor
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p✝ q✝ : Formula α
a✝¹ : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p✝ ↔ p✝ ∈ t.tableau.1
a✝ : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q✝ ↔ q✝ ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ t ⊧ p✝ ⋎ q✝ ↔ p✝ ⋎ q✝ ∈ t.tableau.1
no goals