proposition: Lemma getUnique_eq_inv : forall (A : Set)(a : A)(eqd1 eqd2 : eq_dec A)(ls1 ls2 : list A), getUnique ls1 eqd1 = getUnique ls2 eqd2 -> In a ls1 -> In a ls2.
proof: Proof. induction ls1; intuition; simpl in *; intuition; subst. destruct (in_dec eqd1 a (getUnique ls1 eqd1)). rewrite H in i. apply in_getUnique_if in i. trivial. apply getUnique_cons in H. destruct H. destruct H. intuition. subst. eapply in_or_app. simpl. intuition. destruct (in_dec eqd1 a0 (getUnique ls1 eqd1)). eapply IHls1; intuition. apply getUnique_cons in H. destruct H. destruct H. intuition. subst. apply in_or_app. simpl. right. right. eapply IHls1; intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation