rw [←(hExt hww')]
case neg.h
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
w' : M.Frame.World
hww' : w ≺ w'
⊢ ¬Satisfies M w' p
case neg.h
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
h : ¬w ⊧ p
w' : M.Frame.World
hww' : w ≺ w'
⊢ ¬Satisfies M w p