proposition: Theorem app_eq_app X (x1 x2 y1 y2: list X) : x1++x2 = y1++y2 -> exists l, (x1 = y1++l /\ y2 = l++x2) \/ (y1 = x1++l /\ x2 = l++y2).
proof: Proof. revert y1. induction x1 as [|a x1 IH]. - cbn. intros y1 ->. exists y1. now right. - intros [|b y1]; cbn. + intros <-. exists (a :: x1). now left. + intros [=-> [l Hl] %IH]. exists l. now destruct Hl as [[-> ->]|[-> ->]]; [left|right]. Qed.
imports: PeanoNat