proposition: Lemma matchOrder_NoDup : forall (A : Set)(eqd : eq_dec A)(ls1 ls2 : list A), (forall a, In a ls1 -> In a ls2) -> NoDup ls2 -> NoDup ls1 -> NoDup (matchOrder eqd ls1 ls2).
proof: Proof. induction ls1; intuition; simpl in *. inversion H1; clear H1; subst. econstructor. eapply matchOrder_not_in. intuition. destruct (eqd a a0); subst; intuition. eapply removeFirst_in. eapply H. intuition. intuition. eapply removeFirst_NoDup_not_in; eauto. eapply IHls1; intuition. destruct (eqd a a0); subst; intuition. eapply removeFirst_in; eauto. eapply removeFirst_NoDup; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool