[ unfold Not; intros; destruct H1;
| simplify; intros;
cases (b2pT ? ? (andbPF ? ?) (p2bT ? ? (negbP ?) H)); clear H;
- [ intros; lapply (b2pF ? ? (eqP d ? ?) H1) as H'; clear H1;
+ [ intro; lapply (b2pF ? ? (eqP d ? ?) H1) as H'; clear H1;
destruct H; apply H'; reflexivity;
- | intros; lapply (IH ? H1) as H'; destruct H;
+ | intro; lapply (IH ? H1) as H'; destruct H;
apply H'; reflexivity;]]]]
qed.