proposition: Lemma getUnique_Permutation : forall (A : Set)(eqd1 eqd2 : eq_dec A)(ls1 ls2 : list A), Permutation ls1 ls2 -> Permutation (getUnique ls1 eqd1) (getUnique ls2 eqd2).
proof: Proof. induction 1; intuition; simpl in *. destruct (in_dec eqd1 x (getUnique l eqd1)). destruct (in_dec eqd2 x (getUnique l' eqd2)). eauto. exfalso. eapply n. eapply Permutation_in; eauto. destruct (in_dec eqd2 x (getUnique l' eqd2)). exfalso. eapply n. eapply Permutation_in. eapply Permutation_sym. eauto. eauto. eapply perm_skip. trivial. destruct (in_dec eqd1 x (getUnique l eqd1)). destruct (in_dec eqd1 y (getUnique l eqd1)). destruct (in_dec eqd2 y (getUnique l eqd2)). destruct (in_dec eqd2 x (getUnique l eqd2)). eapply NoDup_Permutation; eauto using getUnique_NoDup; intuition; eauto using in_getUnique, in_getUnique_if. exfalso. eauto using in_getUnique, in_getUnique_if. exfalso. eauto using in_getUnique, in_getUnique_if. destruct (in_dec eqd2 y (getUnique l eqd2)). exfalso. eauto using in_getUnique, in_getUnique_if. destruct (in_dec eqd2 x (y :: getUnique l eqd2)). eapply perm_skip. eapply NoDup_Permutation; eauto using getUnique_NoDup; intuition; eauto using in_getUnique, in_getUnique_if. simpl in *. intuition. exfalso. eauto using in_getUnique, in_getUnique_if. destruct (in_dec eqd1 y (x :: getUnique l eqd1)). destruct (in_dec eqd2 y (getUnique l eqd2)). destruct (in_dec eqd2 x (getUnique l eqd2)). exfalso. eauto using in_getUnique, in_getUnique_if. eapply perm_skip. eapply NoDup_Permutation; eauto using getUnique_NoDup; intuition; eauto using in_getUnique, in_getUnique_if. destruct (in_dec eqd2 x (y :: getUnique l eqd2)). simpl in *; intuition. clear H. subst. eapply perm_skip. eapply NoDup_Permutation; eauto using getUnique_NoDup; intuition; eauto using in_getUnique, in_getUnique_if. subst. exfalso. eauto using in_getUnique, in_getUnique_if. subst. exfalso. eauto using in_getUnique, in_getUnique_if. exfalso. eauto using in_getUnique, in_getUnique_if. simpl in *; intuition; subst. intuition. exfalso. eauto using in_getUnique, in_getUnique_if. destruct (in_dec eqd2 y (getUnique l eqd2)). destruct (in_dec eqd2 x (getUnique l eqd2)). exfalso. eauto using in_getUnique, in_getUnique_if. simpl in n0; intuition. exfalso. eauto using in_getUnique, in_getUnique_if. destruct (in_dec eqd2 x (y :: getUnique l eqd2)). simpl in *; intuition; subst. intuition. exfalso. eauto using in_getUnique, in_getUnique_if. eapply perm_trans. eapply perm_swap. eapply perm_skip. eapply perm_skip. eapply NoDup_Permutation; eauto using getUnique_NoDup; intuition; eauto using in_getUnique, in_getUnique_if. eapply perm_trans. eapply IHPermutation1. eapply (@perm_trans _ _ (getUnique l' eqd1)). eapply NoDup_Permutation; eauto using getUnique_NoDup; intuition; eauto using in_getUnique, in_getUnique_if. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia