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 :: nil) /\ l2 = b :: l4).
proof: Proof. intros l1; elim l1; simpl; 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. case l; simpl. intros H0; right; right; injection H0; split; auto. f_equal; auto. intros b0 l0 H0; left; exists l0; injection H0; intros; (repeat f_equal); auto. intros b0 l0 H0; case (H l2 l0 l4 a0 b); auto. injection H0; auto. intros [l5 HH1]; left; exists l5; f_equal; auto; injection H0; auto. intros [H1|[H1 H2]]; auto. right; right; split; auto; f_equal; auto; injection H0; auto. Qed.
imports: List Arith Tactic Inverse_Image Wf_nat