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