[ intros; lapply (b2pF ? ? (eqP d ? ?) H1) as H'; clear H1;
destruct H; rewrite > Hcut in H'; apply H'; reflexivity;
| intros; lapply (IH ? H1) as H'; destruct H;
[ intros; lapply (b2pF ? ? (eqP d ? ?) H1) as H'; clear H1;
destruct H; rewrite > Hcut in H'; apply H'; reflexivity;
| intros; lapply (IH ? H1) as H'; destruct H;