|Page 310 of 800||Search internet|
A 'proof constructor' is construct like
T proof of L : P
which proves a lemma. The constructor above proves the lemma in the theory using the proof .
We shall refer to the proof constructor above as the T proof constructor as opposed to the plain proof constructor described later.
As an example of a proof constructed by the T proof constructor, take the proof of on the multzero page:
|Page 310 of 800||Search logiweb.eu|