obtain ⟨y, hy₁, hy₂⟩ := by simpa using hC;
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
hC : ¬Satisfies { Frame := F, Valuation := V } xm (□p)
⊢ False
case intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
hC : ¬Satisfies { Frame := F, Valuation := V } xm (□p)
y : F.World
hy₁ : xm ≺ y
hy₂ : ¬Satisfies { Frame := F, Valuation := V } y p
⊢ False