proposition: Lemma no_repeats_app : forall T (l1 l2 : list T), no_repeats (l1 ++ l2) <=> (no_repeats l1 # no_repeats l2 # disjoint l1 l2).
proof: Proof. induction l1; introv; allsimpl; split; intro k; repnd; dands; auto; try (complete sp); allrw no_repeats_cons; repnd; dands; auto; allrw in_app_iff; allrw not_over_or; repnd; dands; auto; allrw disjoint_cons_l; repnd; dands; auto; try (complete (discover; sp)). apply IHl1; sp. Qed.
imports: UsefulTypes bin_rels Omega