r at the end of the
proof box, then the application of the proof rule for
-introduction right after the box
will not type check, not matter how we fill the
remaining part of the box. This is so since the formula
q
r is not a contradiction,
but this is required for the pattern of
-introduction. Consult the summary
of proof rules in Chapter 1 to verify this.