∀n: uuax skipfact_dom. two * n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O).
#n; nelim n; /2/;
#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;