 From this informal structure, the BIO interface can import traditional Natural Deduction, with the introduction and elimination rules, or even a “‘structurally explicit’ sequent to sequent style” version (French 2021: section 3.1) in the fashion of Dummett (1977). Prover then brings forth sequents for Skeptic to accept, and Prover is entitled to state sequents that follow in virtue of the introduction and elimination rules or in virtue of “structural” rules.