|Page 352 of 800||Search internet|
Recall again the proofs of :
In Line L03, the FOL rule unitac sees that is a meta-theorem and thus passes it to the standard rule unitac. Lemma is generalization enriched by a hypothesis :
The number in indicates that the rule performs one generalization. The Peano page also defines and for performing and generalizations, respectively.
In conclusion, the proof expands into something like the following:
|Page 352 of 800||Search logiweb.eu|