proposition: Lemma NoDupA_app : forall l l', NoDupA l -> NoDupA l' -> (forall x, InA x l -> InA x l' -> False) -> NoDupA (l++l').
proof: Proof. intros l; induction l as [|a l IHl]; simpl; auto; intros l' H H0 H1. inv. constructor. - rewrite InA_alt; intros (y,(H4,H5)). destruct (in_app_or _ _ _ H5). + match goal with H2' : ~ InA a l |- _ => rename H2' into H2 end. elim H2. rewrite InA_alt. exists y; auto. + apply (H1 a). * auto. * rewrite InA_alt. exists y; auto. - apply IHl; auto. intros x ? ?. apply (H1 x); auto. Qed.
imports: List Sorted Setoid Basics Morphisms