simp [IntDPCounterexampleFrame] at hWX
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p✝ q✝ : Formula α
M₁ M₂ : Model α
w₁ : M₁.World
w₂ : M₂.World
p q : Formula α
ihp : ∀ {w : M₁.World}, Satisfies M₁ w p ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q
w : M₁.World
h : ∀ {w' : M₁.Frame.World}, w ≺ w' → Satisfies M₁ w' p → Satisfies M₁ w' q
X : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) X p
hWX : (IntDPCounterexampleModel M₁ M₂ w₁ w₂).Frame.Rel (Sum.inr (Sum.inl w)) X
⊢ ∃ x, w ≺ x ∧ Sum.inr (Sum.inl x) = X
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p✝ q✝ : Formula α
M₁ M₂ : Model α
w₁ : M₁.World
w₂ : M₂.World
p q : Formula α
ihp : ∀ {w : M₁.World}, Satisfies M₁ w p ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q
w : M₁.World
h : ∀ {w' : M₁.Frame.World}, w ≺ w' → Satisfies M₁ w' p → Satisfies M₁ w' q
X : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World
hp : Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) X p
hWX :
  match Sum.inr (Sum.inl w), X with
  | Sum.inl val, Sum.inl val_1 => True
  | Sum.inl val, Sum.inr (Sum.inl v) => w₁ ≺ v
  | Sum.inl val, Sum.inr (Sum.inr v) => w₂ ≺ v
  | Sum.inr (Sum.inl w), Sum.inr (Sum.inl v) => w ≺ v
  | Sum.inr (Sum.inr w), Sum.inr (Sum.inr v) => w ≺ v
  | x, x_1 => False
⊢ ∃ x, w ≺ x ∧ Sum.inr (Sum.inl x) = X