proposition: Theorem ulist_incl_length: forall (l1 l2 : list A), ulist l1 -> incl l1 l2 -> le (length l1) (length l2).
proof: Proof. intros l1 l2 H1 Hi; case ulist_incl_permutation with ( 2 := Hi ); auto. intros l3 Hl3; rewrite Permutation_length with ( 1 := Hl3 ); auto. rewrite app_length; simpl; auto with arith. Qed.
imports: List Arith Permutation ListSet