proposition: Theorem in_ex_app: forall (a : A) (l : list A), In a l -> (exists l1 : list A , exists l2 : list A , l = l1 ++ (a :: l2) ).
proof: Proof. intros a l; elim l; clear l; simpl; auto. intros H; case H. intros a1 l H [H1|H1]; auto. exists (nil (A:=A)); exists l; simpl; auto. rewrite H1; auto. case H; auto; intros l1 [l2 Hl2]; exists (a1 :: l1); exists l2; simpl; auto. rewrite Hl2; auto. Qed.
imports: List Arith Tactic Inverse_Image Wf_nat