- #n; nelim n
- [ @1; nnormalize; @1
- | #m; nelim m; nnormalize
- [ #H; @2; nnormalize
- [ //
- | #y; *; #a; #E; nrewrite > E; ncases a; nnormalize; // ]
- ##| #p; #H1; #H2; @2; nnormalize
- [ //
- | #y; *; #a; #E; nrewrite > E; ncases a; nnormalize;
- nrewrite < (plus_n_Sm …); // ]##]
+ #n; nelim n; /2/;
+ #m; nelim m; 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;
+ nrewrite < (plus_n_Sm …); // ]