val term_of_equality: UriManager.uri -> equality -> Cic.term
val term_is_equality: Cic.term -> bool
-val saturate_term : equality_bag -> Cic.metasenv -> Cic.context -> Cic.term ->
+val saturate_term :
+ equality_bag -> Cic.metasenv -> Cic.substitution -> Cic.context -> Cic.term ->
equality_bag * Cic.term * Cic.metasenv * Cic.term list
val push_maxmeta : equality_bag -> int -> equality_bag