proposition: Lemma getUnique_cons : forall (A : Set)(eqd : eq_dec A)(ls2 ls1 : list A) a, a :: ls1 = (getUnique ls2 eqd) -> exists ls3 ls4, ls2 = ls3 ++ (a :: ls4) /\ ls1 = (getUnique ls4 eqd).
proof: Proof. induction ls2; intuition; simpl in *. inversion H. destruct (in_dec eqd a (getUnique ls2 eqd)). apply IHls2 in H. destruct H. destruct H. intuition. subst. econstructor. econstructor. split. eapply app_comm_cons. trivial. inversion H; clear H; subst. econstructor. econstructor. intuition. rewrite app_nil_l. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation