- ##[ ##1: nnormalize; #H1;
- ndestruct (*napply (bool_destruct … H1)*)
- ##| ##2: #yy; nnormalize; #H1; #H2;
- (* !!! ndestruct: assert false *)
- napply (option_destruct_none_some T … H2)
+ ##[ ##1: nnormalize; #f; #H; #H1; napply (bool_destruct … H1)
+ ##| ##2: #yy; #f; #H; nnormalize; #H1; #H2; napply (option_destruct_none_some T … H2)