proposition: Lemma getUnique_NoDup : forall (A : Set)(ls : list A)(eqd: eq_dec A), NoDup (getUnique ls eqd).
proof: Proof. induction ls; intuition; simpl in *. econstructor. destruct (in_dec _ a (getUnique ls _)); eauto. econstructor; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation