- [ #_; #H; napply refl; nauto
- | #H; #_; ncut (uuC … b=uuC … b) [nauto] ncases (uuC … b) in ⊢ (???% → ?)
- [ #E; napply False_rect_Type0; ncut (b=b) [nauto] ncases p in ⊢ (???% → ?)
- [ #a; #K; #E2; napply H [ nauto | nrewrite > E2; nauto ]
+ [ #_; #H; napply refl; /2/
+ | #H; #_; ncut (uuC … b=uuC … b) [//] ncases (uuC … b) in ⊢ (???% → ?)
+ [ #E; napply False_rect_Type0; ncut (b=b) [//] ncases p in ⊢ (???% → ?)
+ [ #a; #K; #E2; napply H [ // | nrewrite > E2; // ]