proposition: Lemma matchOrder_permutation : forall (A : Set)(eqd : eq_dec A)(ls1 ls2 : list A), NoDup ls1 -> NoDup ls2 -> (forall a, In a ls1 -> In a ls2) -> Permutation ls2 (matchOrder eqd ls1 ls2).
proof: Proof. intuition. eapply NoDup_Permutation; intuition. eapply matchOrder_NoDup; eauto. eapply (@matchOrder_In _ eqd ls1 ls2); eauto. eapply (@matchOrder_In _ eqd ls1 ls2); eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation