apply not_imp_not.mpr trivTranslated_of_K4
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ⊬! Axioms.L (atom default)
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ⊢! (Axioms.L (atom default)ᵀᴾ) ⋯