dsimp only [Axioms.K, VerTranslation, toPropFormula]
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐆𝐋 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐂𝐥 ⊢! (Axioms.K w✝¹ w✝ⱽᴾ) ⋯
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐆𝐋 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐂𝐥 ⊢! ⊤ ⟶ ⊤ ⟶ ⊤