proposition: Theorem ulist_eq_permutation: forall (l1 l2 : list A), ulist l1 -> incl l1 l2 -> length l1 = length l2 -> permutation l1 l2.
proof: Proof. intros l1 l2 H1 H2 H3. case (ulist_incl_permutation l1 l2); auto. intros l3 H4. assert (H5: l3 = @nil A). generalize (permutation_length _ _ _ H4); rewrite length_app; rewrite H3. rewrite Nat.add_comm; case l3; simpl; auto. intros a l H5; absurd (lt (length l2) (length l2)); auto with arith. pattern (length l2) at 2; rewrite H5; auto with arith. replace l1 with (app l1 l3); auto. apply permutation_sym; auto. rewrite H5; rewrite app_nil_end; auto. Qed.
imports: List Arith Permutation ListSet