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