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. intros l1 l2 H1 Hi Hi0; case ulist_incl_permutation with ( 2 := Hi ); auto. intros l3 Hl3; rewrite permutation_length with ( 1 := Hl3 ); auto. rewrite length_app; simpl; auto with arith. generalize Hl3; case l3; simpl; auto with arith. rewrite <- app_nil_end; auto. intros H2; case Hi0; auto. intros a HH; apply permutation_in with ( 1 := H2 ); auto. intros a l Hl0; (rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; auto with arith). Qed.
imports: List Arith Permutation ListSet