(* returns: (carr,menv,(saturated coercion,last arg)option,idem) list *)
val meets :
Cic.metasenv -> Cic.substitution -> Cic.context ->
(* returns: (carr,menv,(saturated coercion,last arg)option,idem) list *)
val meets :
Cic.metasenv -> Cic.substitution -> Cic.context ->