intro hCF
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
⊢ ¬ConverseWellFounded F.Rel → ¬F ⊧* 𝗟
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
⊢ ¬F ⊧* 𝗟