NCic.term -> NCic.term -> NCic.term -> int -> int -> 'status
(* NOTE: the name of the coercion is used to sort coercions, thus
NCic.term -> NCic.term -> NCic.term -> int -> int -> 'status
(* NOTE: the name of the coercion is used to sort coercions, thus