proposition: Theorem app_decompose : forall (A:Type) (l1 l2 l3 l4:list A), l1 ++ l2 = l3 ++ l4 -> (exists l1' : list A, l1 = l3 ++ l1' /\ l4 = l1' ++ l2) \/ (exists a : A, exists l2' : list A, l3 = l1 ++ a :: l2' /\ l2 = (a :: l2') ++ l4).
proof: Proof. simple induction l1. - intros l2 l3; case l3. + intros l4 H; left; exists (nil (A:=A)); auto. + intros a l3' Heq; right; exists a; exists l3'; auto. - clear l1; intros a l1 Hrec l2 l3; case l3. + intros l4 H; left; exists (a :: l1); auto. + simpl ; intros a' l3' l4 Heq; injection Heq; intros Heq' Heq''. elim Hrec with (1 := Heq'). intros [l1' [Heq3 Heq4]]; left; exists l1'; split; auto. rewrite Heq''; rewrite Heq3; auto. intros [a'' [l2' [Heq3 Heq4]]]; right; exists a'', l2'; split; auto. rewrite Heq''; rewrite Heq3; auto. Qed.
imports: List Arith