+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
+val maxmeta : equality_bag -> int
+val filter_metasenv_gt_maxmeta: equality_bag -> Cic.metasenv -> Cic.metasenv
+