. apply reducible_K4_GL;
case left
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ≤ₛ 𝐆𝐋

case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐆𝐋 ≤ₛ 𝐊𝟒
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐆𝐋 ≤ₛ 𝐊𝟒