. simp [System.not_reducible_iff];
  existsi (Axioms.L (atom default))
  constructor;
  . exact axiomL!;
  . exact unprovable_AxiomL_K4;
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐆𝐋 ≤ₛ 𝐊𝟒
no goals