simp [System.not_reducible_iff]
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐆𝐋 ≤ₛ 𝐊𝟒
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ f, 𝐆𝐋 ⊢! f ∧ 𝐊𝟒 ⊬! f