Non-contingency logic replaces the standard necessity operator with an operator expressing that a statement has the same truth value in all accessible worlds, meaning it is either necessarily true or necessarily false. While this logic has been studied semantically, the question of whether it possesses an intrinsic, well-behaved proof system in the form of a cut-free sequent calculus that does not pass through a detour via classical modal logic S5 or similar systems remains unresolved. The challenge is to find inference rules that capture the peculiar non-self-dual character of the non-contingency operator directly at the syntactic level.