val metas_of_term: Cic.term -> int list
val metas_of_proof: proof -> int list
(** ensures that metavariables in equality are unique *)
val fix_metas: int -> equality -> int * equality
val metas_of_term: Cic.term -> int list
val metas_of_proof: proof -> int list
(** ensures that metavariables in equality are unique *)
val fix_metas: int -> equality -> int * equality