proposition: Lemma noduplicates_of_list_repr : forall E xs, list_repr E xs -> noduplicates xs.
proof: Proof. Proof using. unfold list_repr. tauto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)