proposition: Lemma bnodup_ok : forall l, bnodup l = true <-> nodup l.
proof: Proof. induction l; simpl; intros. tauto. rewrite andb_eq. rewrite IHl. rewrite <- (mem_ok beq_ok). rewrite negb_lr. simpl. rewrite false_not_true. refl. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)