The hypothesis rule, also known as the assumption rule. It states that the initial sequent A ⊢ A may be introduced, i.e. derived from zero premises. The seemingly useless conjunction with the verum ⊤ is an artifact of the way the proof verifier works; it does not occur in proof notation and can be ignored. The derivation system stated by the rules is sequent natural deduction. In this regard, the assumption made by the hypothesis rule appears as a dependency that can later be uncharged by subj_intro or neg_intro.