#y; *; #a; #E; nrewrite > E; ncases a; nnormalize; //
##| #p; #H1; #H2; @2; nnormalize; //;
#y; *; #a; #E; nrewrite > E; ncases a; nnormalize;
#y; *; #a; #E; nrewrite > E; ncases a; nnormalize; //
##| #p; #H1; #H2; @2; nnormalize; //;
#y; *; #a; #E; nrewrite > E; ncases a; nnormalize;