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

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