proposition: Theorem in_permutation_ex : forall a l, In a l -> exists l1 : list A, permutation (a :: l1) l.
proof: Proof. intros a l; elim l; simpl in |- *; auto. intros H; case H; auto. intros a0 l0 H [H0| H0]. exists l0; rewrite H0; auto. case H; auto; intros l1 Hl1; exists (a0 :: l1). apply permutation_trans with (a0 :: a :: l1); auto. Qed.
imports: List ListAux