for questions or link request: module admin

Substitution of Proof Lines

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


This module declares the general rule for substituting variables.


This document uses the results of the following documents:


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: