proposition: Lemma Listing_decidable_eq {A:Type} (l:list A): Listing l -> decidable_eq A.
proof: Proof. intros (Hnodup & Hfull) a a'. now apply (NoDup_list_decidable Hnodup). Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec