val refl_proof: UriManager.uri -> Cic.term -> Cic.term -> Cic.term
(** ensures that metavariables in equality are unique *)
val fix_metas_goal: int -> goal -> int * goal
val refl_proof: UriManager.uri -> Cic.term -> Cic.term -> Cic.term
(** ensures that metavariables in equality are unique *)
val fix_metas_goal: int -> goal -> int * goal