Consider the classical propositional calculus over the alphabet $\{\bot,\top,\neg,\land,\lor,\rightarrow\}$ with the following inference rules (together with the initial sequent):
Is cut-elimination for this particular calculus proved somewhere in the literature? All I could find were proofs for calculi without the $0$-ary connectives $\bot$ and $\top$.