#
Substitution of Proof Lines

name: subst, module version: 1.00.00, rule version: 1.01.00, original: subst, author of this module: Michael Meyling
## Description

This module declares the general rule for substituting variables.
## References

This document uses the results of the following documents:
## Content

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.

## Cross References

This document is used by the following documents: