| Theorem of thm_flavour * string option * 'term * 'term option
(* flavour, name, type, body
* - name is absent when an unnamed theorem is being proved, tipically in
| Theorem of thm_flavour * string option * 'term * 'term option
(* flavour, name, type, body
* - name is absent when an unnamed theorem is being proved, tipically in