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.

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**.