(** parameters, list of loc * mutual inductive types *)
| Theorem of Cic.object_flavour * string * term * term option
(** flavour, name, type, body
* - name is absent when an unnamed theorem is being proved, tipically in
* interactive usage
* - body is present when its given along with the command, otherwise it
(** parameters, list of loc * mutual inductive types *)
| Theorem of Cic.object_flavour * string * term * term option
(** flavour, name, type, body
* - name is absent when an unnamed theorem is being proved, tipically in
* interactive usage
* - body is present when its given along with the command, otherwise it