existsi xm
case intro.intro.intro.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
⊢ ∃ x,
    w ≺ x ∧
      (∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := V } w' p) ∧
        ¬Satisfies { Frame := F, Valuation := V } x p
case intro.intro.intro.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
⊢ w ≺ xm ∧
    (∀ (w' : F.World), xm ≺ w' → Satisfies { Frame := F, Valuation := V } w' p) ∧
      ¬Satisfies { Frame := F, Valuation := V } xm p