proposition: Theorem ulist_perm: forall (l1 l2 : list A), permutation l1 l2 -> ulist l1 -> ulist l2.
proof: Proof. intros l1 l2 H; elim H; clear H l1 l2; simpl; auto. intros a l1 l2 H0 H1 H2; apply ulist_cons; auto. inversion_clear H2 as [|ia il iH1 iH2 [iH3 iH4]]; auto. intros H3; case iH1; apply permutation_in with ( 1 := permutation_sym _ _ _ H0 ); auto. inversion H2; auto. intros a b L H0; apply ulist_cons; auto. inversion_clear H0 as [|ia il iH1 iH2]; auto. inversion_clear iH2 as [|ia il iH3 iH4]; auto. intros H; case H; auto. intros H1; case iH1; rewrite H1; simpl; auto. apply ulist_cons; auto. inversion_clear H0 as [|ia il iH1 iH2]; auto. intros H; case iH1; simpl; auto. inversion_clear H0 as [|ia il iH1 iH2]; auto. inversion iH2; auto. Qed.
imports: List Arith Permutation ListSet