- Cic.term -> Cic.term -> Cic.context ->
- Cic.metasenv -> CicUniv.universe_graph -> int (* arity *) ->
- bool (* last lambda goes with innermost arg *) ->
+ Cic.term -> Cic.term (* t2 *) -> Cic.context ->
+ Cic.metasenv -> CicUniv.universe_graph ->
+ int -> int (* saturations of t1/t2 *) ->