proposition: Lemma equivlistA_NoDupA_split l l1 l2 x y : eqA x y -> NoDupA (x::l) -> NoDupA (l1++y::l2) -> equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2).
proof: Proof. intros H H0 H1 H2; intro a. generalize (H2 a). rewrite !InA_app_iff, !InA_cons. inv. assert (SW:=NoDupA_swap H1). inv. rewrite InA_app_iff in *. split; intros. - match goal with H3 : ~ InA x l |- _ => assert (~eqA a x) by (contradict H3; rewrite <- H3; auto) end. assert (~eqA a y) by (rewrite <- H; auto). tauto. - assert (OR : eqA a x \/ InA a l) by intuition. destruct OR as [EQN|INA]; auto. match goal with H0 : ~ (InA y l1 \/ InA y l2) |- _ => elim H0 end. rewrite <-H,<-EQN; auto. Qed.
imports: List Sorted Setoid Basics Morphisms