let rec aux f = function
| ESort -> f ESort
| EBind (e, a, Abst (r, n, w)) -> aux (push_bind f a (Abst (r, n0, w))) e
| EBind (e, a, b) -> aux (push_bind f a b) e
| EAppl (e, a, x, v) -> aux (push_appl f a x v) e
| EProj (e, a, d) -> let f d = aux (push_proj f a d) e in aux f d
let rec aux f = function
| ESort -> f ESort
| EBind (e, a, Abst (r, n, w)) -> aux (push_bind f a (Abst (r, n0, w))) e
| EBind (e, a, b) -> aux (push_bind f a b) e
| EAppl (e, a, x, v) -> aux (push_appl f a x v) e
| EProj (e, a, d) -> let f d = aux (push_proj f a d) e in aux f d