proposition: Theorem in_getUnique : forall (A : Set)(ls : list A)(eqd : eq_dec A) a, In a ls -> In a (getUnique ls eqd).
proof: Proof. induction ls; simpl in *; intuition. subst. destruct (in_dec _ a0 (getUnique ls _)); simpl; auto. destruct (in_dec _ a (getUnique ls _)); simpl. eapply IHls. trivial. right. eapply IHls. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation