If a proof line could be derived by using rule4 (rename proposition variable), predrule1 (rename bound subject variable) and predrule2 (rename free subject variable) multiple times, we declare a new rule to shorten that derivation:
1. Rule Declaration
Substitute Variables (rule8)
The use of this rule could always be replaced by proof lines that make only use of the referenced rules.