apply not_imp_not.mpr verTranslated_of_GL
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊬! Axioms.T (atom default)
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ⊢! (Axioms.T (atom default)ⱽᴾ) ⋯