proposition: Lemma split_list : forall (A : Type) (l1 l2 l3 l4 : list A), l1 ++ l2 = l3 ++ l4 -> {l | l1 = l3 ++ l /\ l4 = l ++ l2} + {l | l3 = l1 ++ l /\ l2 = l ++ l4}.
proof: Proof. intros A l1; induction l1 as [ | a1 l1]. right; exists l3; split; trivial. intros l2 [ | a3 l3] l4 H. left; exists (a1 :: l1); split; trivial. rewrite H; trivial. injection H; clear H; intros H a1_eq_a3; subst a3. destruct (IHl1 _ _ _ H) as [H' | H']. destruct H' as [l [H1 H2]]; subst l1 l4. left; exists l; split; trivial. destruct H' as [l [H1 H2]]; subst l2 l3. right; exists l; split; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)