proposition: Lemma matchOrder_In : forall (A : Set)(eqd : eq_dec A)(ls1 ls2 : list A), NoDup ls1 -> NoDup ls2 -> (forall a, In a ls1 -> In a ls2) -> (forall a, In a ls2 <-> In a (matchOrder eqd ls1 ls2)).
proof: Proof. induction ls1; destruct ls2; intuition; simpl in *; eauto; intuition; subst. inversion H; clear H; subst. inversion H0; clear H0; subst. destruct (eqd a a1); subst. intuition. right. eapply (IHls1 (a1 :: removeFirst _ ls2 a)); intuition. econstructor. eapply removeFirst_not_in; intuition. eapply removeFirst_NoDup; intuition. simpl. destruct (H1 a0); auto. right. eapply removeFirst_in; eauto. intuition. subst. intuition. inversion H; clear H; subst. inversion H0; clear H0; subst. destruct (H1 a); intuition; subst. destruct (eqd a a); try congruence. right. eapply (IHls1 ls2); intuition. destruct (H1 a0); intuition; subst. intuition. destruct (eqd a a0); try congruence. destruct (eqd a a1); subst; auto. right. eapply (IHls1 (a0 :: removeFirst _ ls2 a)); intuition. econstructor. eapply removeFirst_not_in; trivial. eapply removeFirst_NoDup; trivial. simpl. destruct (H1 a2); eauto. destruct (eqd a0 a2); intuition. right. eapply removeFirst_in; trivial. intuition. subst. intuition. simpl. destruct (eqd a0 a1); intuition. right. eapply removeFirst_in; trivial. intuition. inversion H; clear H; subst. inversion H0; clear H0; subst. destruct (eqd a0 a1); subst; intuition. right. assert (In a1 (if eqd a a0 then ls2 else a0 :: removeFirst eqd ls2 a)). eapply IHls1. trivial. destruct (eqd a a0). trivial. econstructor. eapply removeFirst_not_in; eauto. eapply removeFirst_NoDup; intuition. intuition. destruct (eqd a a0). destruct (H1 a2). intuition. subst. intuition. trivial. simpl. destruct (eqd a0 a2); intuition. right. destruct (H1 a2). destruct (eqd a a2); intuition. subst. intuition. eapply removeFirst_in. trivial. intuition. subst. intuition. trivial. destruct (eqd a a0); intuition. simpl in *. intuition. eapply removeFirst_in_iff. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool