proposition: Theorem norep_disj_appP l1 l2: no_repeatsP l1 -> no_repeatsP l2 -> disjointP l1 l2 -> no_repeatsP (l1 ++ l2).
proof: Proof. elim: l1=>//= x xs Hi H1 H2 H3; split; first last. - by apply: Hi=>//; [case: H1=>// | case: H3=>//]. rewrite appears_in_appP. by case; [case: H1| case: H3]. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq)