proposition: Lemma no_repeat_dec: forall A, forall eq : Deq A, forall l : list A, decidable (no_repeats l).
proof: Proof. intros. induction l; cpx. destruct (in_deq _ eq a l);[right | ]. - introv Hin. inverts Hin; cpx. - destruct IHl; [left; constructor; trivial| right]. introv Hnt. inverts Hnt; cpx. Defined.
imports: UsefulTypes bin_rels Omega