proposition: Theorem split_one_in_ex : forall (a : A) (l1 : list A), In a l1 -> exists l2 : list A, In (a, l2) (split_one l1).
proof: Proof. intros a l1; elim l1; simpl in |- *; auto. intros H; case H. intros a0 l H [H0| H0]; auto. exists l; left; apply f_equal2 with (f := pair (A:=A) (B:=list A)); auto. case H; auto. intros x H1; exists (a0 :: x); right; auto. apply (in_map (fun p : A * list A => (fst p, a0 :: snd p)) (split_one l) (a, x)); auto. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)