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