proposition: Theorem in_ex_app_first: forall (a : A) (l : list A), In a l -> (exists l1 : list A , exists l2 : list A , l = l1 ++ (a :: l2) /\ ~ In a l1 ).
proof: Proof. intros a l; elim l; clear l; auto. intros H; case H. intros a1 l H H1; auto. generalize (in_inv_dec _ _ _ H1); intros [H2|[H2 H3]]. exists (nil (A:=A)); exists l; simpl; split; auto. subst; auto. case H; auto; intros l1 [l2 [Hl2 Hl3]]; exists (a1 :: l1); exists l2; simpl; split; auto. subst; auto. intros H4; case H4; auto. Qed.
imports: List Arith Permutation ListSet