 Gentzen’s method for natural deduction—his \(\mathcal{N}\) calculi—were given in a tree format with occurrences of formulas appearing as nodes of the tree. The root of the tree is the formula to be proved, and the “suppositions” are at the leaves of the tree. The following is such a proof tree for the theorem