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