proposition: Theorem permutation_cons_ex : forall (a : A) (l1 l2 : list A), permutation (a :: l1) l2 -> exists l3 : list A, (exists l4 : list A, l2 = l3 ++ a :: l4 /\ permutation l1 (l3 ++ l4)).
proof: Proof. intros a l1 l2 H. apply (permutation_cons_ex_aux a (a :: l1) l2 H nil l1); simpl in |- *; auto. Qed.
imports: List ListAux