5.8ex II

The following are more difficult applications of SD+.

The '/' shortcut works for rules of inference and may be of some help for rules of replacement (for these '/' just rewrites the cited line and lets you make the replacement).