proposition: Lemma getUnique_NoDup_eq : forall (A : Set)(eqd : eq_dec A)(ls : list A), NoDup ls -> getUnique ls eqd = ls.
proof: Proof. induction ls; intuition; simpl in *. inversion H; clear H; subst. destruct (in_dec eqd a (getUnique ls eqd)). exfalso. apply H2. eapply in_getUnique_if. eauto. f_equal. eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia