proposition: Theorem ulist_incl_length_strict: forall (l1 l2 : list A), ulist l1 -> incl l1 l2 -> ~ incl l2 l1 -> lt (length l1) (length l2).
proof: Proof. Proof with auto with arith. intros l1 l2 H1 Hi Hi0; case ulist_incl_permutation with ( 2 := Hi )... intros l3 Hl3; rewrite Permutation_length with ( 1 := Hl3 )... rewrite app_length; simpl... generalize Hl3; case l3; simpl... rewrite <- app_nil_end... intros H2; case Hi0... intros a HH; apply Permutation_in with ( 1 := H2 )... intros a l Hl0; (rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; auto with arith). Qed.
imports: List Arith Permutation ListSet