(** [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 *)
(** [fresh_subst metasenv context uris] takes in input a list of uri and
creates a fresh explicit substitution *)
val fresh_subst:
Cic.metasenv ->
(** [fresh_subst metasenv context uris] takes in input a list of uri and
creates a fresh explicit substitution *)
val fresh_subst:
Cic.metasenv ->