Page 352 of 800
| 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 |