proposition: Lemma unique_app (A: Type) (l1 l2: list A) : unique (l1 ++ l2) -> unique l1.
proof: Proof. elim l1; clear l1. - intros; apply uniqN. - intros a l1 Hrec H; inversion_clear H as [| xx yy Ha Hb]. apply uniqC; auto with datatypes. Qed.
imports: ZArith List