Usual mathematical practice is to first say what you are proving, and then providing a proof for that. Currently there is no way to do this in ProofScript. To do this, a theorem statement
will be introduced which has the syntax:
theorem [optional_name = ] <term>
<proof>
Here proof is supposed to be resulting in a theorem which is supposed to equal term (after context lifting).
Usual mathematical practice is to first say what you are proving, and then providing a proof for that. Currently there is no way to do this in ProofScript. To do this, a theorem statement will be introduced which has the syntax:
Here proof is supposed to be resulting in a theorem which is supposed to equal term (after context lifting).