simp [AxiomSet.L, Axioms.L]
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
⊢ F ⊧* 𝗟
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
⊢ ∀ (a : Formula α), ValidOnFrame F (□(□a ⟶ a) ⟶ □a)