fact: Fixpoint matchOrder (A : Set)(eqd : eq_dec A)(ls1 ls2 : list A) := match ls1 with | nil => ls2 | a :: ls1' => a :: (matchOrder eqd ls1' (removeFirst eqd ls2 a)) end.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool