+(*
+let rec set_name_y f = function
+ | D.ESort -> f D.ESort
+ | D.EBind (e, a, y, b) -> set_name_y (D.push_bind f a {y with E.b_name = Some ("Y", true)} b) e
+ | D.EAppl (e, x, v) -> set_name_y (D.push_appl f x v) e
+ | D.EProj (e, d) -> let f d = set_name_y (D.push_proj f d) e in set_name_y f d
+*)