[1: generalize in match H2; simplify in H2;
lapply (b2pT ? ? (orbP ? ?) H2) as H3; clear H2;
cases H3; clear H3; intros;
[2: lapply (uniq_mem ? ? ? H1) as H4; simplify; apply (cmpP d x t);
intros (H5); simplify;
[1: rewrite > count_O; [reflexivity]
[1: generalize in match H2; simplify in H2;
lapply (b2pT ? ? (orbP ? ?) H2) as H3; clear H2;
cases H3; clear H3; intros;
[2: lapply (uniq_mem ? ? ? H1) as H4; simplify; apply (cmpP d x t);
intros (H5); simplify;
[1: rewrite > count_O; [reflexivity]