proposition: Lemma elements_3w : forall m (Hm:Sort m), NoDupA (elements m).
proof: Proof. intros. apply Sort_NoDupA. apply elements_3; auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses