# %prove

From The Twelf Project

The ** %prove** directive attempts to prove a theorem specified by a

`%theorem`directive using the theorem prover. It is therefore similar to the

`%establish`directive. However, unlike the

`%establish`directive, theorems shown to be true by the

`%prove`directive are considered as potential lemmas when the theorem prover attempts to prove future theorems.