(function _::x::_ -> x | _ -> assert false) n
(CicNotationPres.mpres_of_box bobj)
)
| G.Procedural depth ->
let obj = ProceduralOptimizer.optimize_obj obj in
let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
(function _::x::_ -> x | _ -> assert false) n
(CicNotationPres.mpres_of_box bobj)
)
| G.Procedural depth ->
let obj = ProceduralOptimizer.optimize_obj obj in
let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in