 Clearly, a proof of B is already contained in the given derivation. Proofs without detours are called normal, and Gentzen showed that any proof can be effectively transformed via “reduction steps” into a normal one.