proposition: Theorem app_inv_app: forall l1 l2 l3 l4 a, l1 ++ l2 = l3 ++ (a :: l4) -> (exists l5 : list A , l1 = l3 ++ (a :: l5) ) \/ (exists l5 , l2 = l5 ++ (a :: l4) ).
proof: Proof. intros l1; elim l1; simpl; auto. intros l2 l3 l4 a H; right; exists l3; auto. intros a l H l2 l3 l4 a0; case l3; simpl. intros H0; left; exists l; f_equal; injection H0; auto. intros b l0 H0; case (H l2 l0 l4 a0); auto. injection H0; auto. intros [l5 H1]. left; exists l5; f_equal; injection H0; auto. Qed.
imports: List Arith Tactic Inverse_Image Wf_nat