proposition: Theorem ulist_incl2_permutation: forall (l1 l2 : list A), ulist l1 -> ulist l2 -> incl l1 l2 -> incl l2 l1 -> Permutation l1 l2.
proof: Proof. intros l1 l2 H1 H2 H3 H4. apply ulist_eq_permutation; auto. apply Nat.le_antisymm; apply ulist_incl_length; auto. Qed.
imports: List Arith Permutation ListSet