- | EBind (e, a, y, Abst (r, n, w)) -> aux (push_bind f a y (Abst (r, n0, w))) e
- | EBind (e, a, y, b) -> aux (push_bind f a y b) e
- | EAppl (e, x, v) -> aux (push_appl f x v) e
+ | EBind (e, y, a, Abst (r, n, w)) -> aux (push_bind f y a (Abst (r, n0, w))) e
+ | EBind (e, y, a, b) -> aux (push_bind f y a b) e
+ | EAppl (e, a, v) -> aux (push_appl f a v) e