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 in |- *; auto. intros l2 l3 l4 a H; right; exists l3; auto. intros a l H l2 l3 l4 a0; case l3; simpl in |- *. intros H0; left; exists l; apply f_equal2 with (f := cons (A:=A)); injection H0; auto. intros b l0 H0; case (H l2 l0 l4 a0); auto. injection H0; auto. intros (l5, H1). left; exists l5; apply f_equal2 with (f := cons (A:=A)); injection H0; auto. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)