Error in Example
Example 76.1. is supposed to show an application of the onepoint rule. However, the proof is closed with a qnt_simplify rule (which is not supposed to close a subproof.
Example 76.1. is supposed to show an application of the onepoint rule. However, the proof is closed with a qnt_simplify rule (which is not supposed to close a subproof.