proposition: Theorem app_inv_app2 : forall l1 l2 l3 l4 a b, l1 ++ l2 = l3 ++ a :: b :: l4 -> (exists l5 : list A, l1 = l3 ++ a :: b :: l5) \/ (exists l5, l2 = l5 ++ a :: b :: l4) \/ l1 = l3 ++ a :: [] /\ l2 = b :: l4.
proof: Proof. intros l1; elim l1; simpl in |- *; auto. intros l2 l3 l4 a b H; right; left; exists l3; auto. intros a l H l2 l3 l4 a0 b; case l3; simpl in |- *. case l; simpl in |- *. intros H0; right; right; injection H0; split; auto. apply f_equal2 with (f := cons (A:=A)); auto. intros b0 l0 H0; left; exists l0; injection H0; intros; repeat apply f_equal2 with (f := cons (A:=A)); auto. intros b0 l0 H0; case (H l2 l0 l4 a0 b); auto. injection H0; auto. intros (l5, HH1); left; exists l5; apply f_equal2 with (f := cons (A:=A)); auto; injection H0; auto. intros [H1| (H1, H2)]; auto. right; right; split; auto; apply f_equal2 with (f := cons (A:=A)); auto; injection H0; auto. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)