proposition: Theorem ulist_incl_permutation: forall (l1 l2 : list A), ulist l1 -> incl l1 l2 -> (exists l3 , permutation l2 (l1 ++ l3) ).
proof: Proof. intros l1; elim l1; simpl; auto. intros l2 H H0; exists l2; simpl; auto. intros a l H l2 H0 H1; auto. case (in_permutation_ex _ a l2); auto with datatypes. intros l3 Hl3. case (H l3); auto. apply ulist_inv with ( 1 := H0 ); auto. intros b Hb. assert (H2: In b (a :: l3)). apply permutation_in with ( 1 := permutation_sym _ _ _ Hl3 ); auto with datatypes. simpl in H2 |-; case H2; intros H3; simpl; auto. inversion_clear H0 as [|c lc Hk1]; auto. case Hk1; subst a; auto. intros l4 H4; exists l4. apply permutation_trans with (a :: l3); auto. apply permutation_sym; auto. Qed.
imports: List Arith Permutation ListSet