[ @2; nnormalize; //; #y; *; #a; ncases a
|
#m; nelim m; nnormalize
- [ #H; @2; nnormalize; //;
+ [ #H; @2; nnormalize; ##[//;##] (* XXX: bug auto *)
#y; *; #a; #E; nrewrite > E; ncases a; nnormalize; //
##| #p; #H1; #H2; @2; nnormalize; //;
#y; *; #a; #E; nrewrite > E; ncases a; nnormalize;