proposition: Lemma unique_perm (A : Type) (l1 l2 : list A) : perm l1 l2 -> unique l1 -> unique l2.
proof: Proof. intro H; elim H; clear l1 l2 H; auto. - intros a b l H; inversion_clear H as [| xx yy Ha Hb]. inversion_clear Ha as [| xx uu Ha1 Hb1]. repeat apply uniqC; auto with datatypes. simpl; intros [H1 | H1]; subst; auto with datatypes. - intros a l1 l2 H1 H2 H3. inversion_clear H3 as [| xx yy Ha Hb]. apply uniqC; auto with datatypes. contradict Hb; generalize Hb; elim H1; clear l1 l2 H1 H2 Ha Hb; auto with datatypes. * simpl; intros a1 b1 l [H1 | [H1 | H1]]; auto. * simpl; intros a1 l1 l2 H Hrec [H1 | H1]; auto. Qed.
imports: ZArith List