-N (((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) (((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)))\r
- ((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c))))\r
- (((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c))\r
- (((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a))\r
- ((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))\r
-\r
-$! p32\r
-N (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y)))\r
- (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a)\r
- (((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v)))\r
- ((((a y) v) (z a)) (z (((z a) (z a)) (w. v))))\r
- ((((w (a. (z. ((z a) (z a))))) (v. ((a y) v))) (((z a) (z a)) b)) (w. (((z a) (z a)) (c. (c ((z a) (z a)))))))\r
+N (((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) (((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c))) Z\r
+ ((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) Z\r
+ (((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c)) Z\r
+ (((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) Z\r
+ ((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w)) Z\r
+\r
+$? p32\r
+# should fail because the first and second terms are eta-eq\r
+N (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y))) Z\r
+ (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a) Z\r
+ (((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v))) Z\r
+ ((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) Z\r
+ ((((w (a. (z. ((z a) (z a))))) (v. ((a y) v))) (((z a) (z a)) b)) (w. (((z a) (z a)) (c. (c ((z a) (z a))))))) Z\r