proposition: Lemma matchOrder_not_in : forall (A : Set)(eqd : eq_dec A)(ls1 ls2 : list A) a, (forall a, In a ls1 -> In a ls2) -> ~In a ls2 -> ~In a (matchOrder eqd ls1 ls2).
proof: Proof. induction ls1; intuition; simpl in *. destruct (eqd a a0); subst; intuition. eapply IHls1. intuition. eapply H0. assert (~ In a0 ls1). intuition. specialize (@matchOrder_not_in_h _ eqd ls1 (removeFirst eqd ls2 a) a0); intuition. exfalso. eapply H4; eauto. intuition. eapply removeFirst_not_in. intuition. eapply H0. eapply H5. eapply H3. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool