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.

lemma f: T ≝ t

Same as theorem f: T ≝ t

fact f: T ≝ t

Same as theorem f: T ≝ t

remark f: T ≝ t

Same as theorem f: T ≝ t