simp_all [IntDPCounterexampleModel, Satisfies.iff_models, Satisfies]
case hor
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
w₁ : M₁.World
w₂ : M₂.World
p✝ q✝ : Formula α
a✝¹ : ∀ {w : M₁.World}, Satisfies M₁ w p✝ ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) p✝
a✝ : ∀ {w : M₁.World}, Satisfies M₁ w q✝ ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q✝
w : M₁.World
⊢ Satisfies M₁ w (p✝ ⋎ q✝) ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) (p✝ ⋎ q✝)
no goals