(** [mk_implicit metasenv context]
* add a fresh metavariable to the given metasenv, using given context
* @return the new metasenv and the index of the added conjecture *)
(** [mk_implicit metasenv context]
* add a fresh metavariable to the given metasenv, using given context
* @return the new metasenv and the index of the added conjecture *)