+ (*CSC: here unsharing is necessary to avoid an unwanted
+ relocalization. However, this also shows a great source of
+ inefficiency: "x" is refined twice (once now and once in the
+ subsequent eat_prods_and_args). Morevoer, how is divergence avoided?
+ *)
+ type_of_aux subst metasenv context (Unshare.unshare x) ugraph