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