Matita Home

`theorem f: P ≝ p`

Proves a new theorem **f** whose thesis is
**P**.

If **p** is provided, it must be a proof term for
**P**. Otherwise an interactive proof is started.

**P** can be omitted only if the proof is not
interactive.

Proving a theorem already proved in the library is an error.
To provide an alternative name and proof for the same theorem, use
**variant f: P ≝ p**.

A warning is raised if the name of the theorem cannot be obtained by mangling the name of the constants in its thesis.

Notice that the command is equivalent to **definition f: T ≝ t**.

`variant f: T ≝ t`

Same as **theorem f: T ≝ t**, but it does not
complain if the theorem has already been proved. To be used to give
an alternative name or proof to a theorem.