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