proposition: Lemma split_map_set : forall (A B : Type) (f : A -> B) l l1 l2, map f l = l1 ++ l2 -> {k1 : list A & {k2 : list A | l = k1 ++ k2 /\ map f k1 = l1 /\ map f k2 = l2}}.
proof: Proof. fix split_map_set 4. intros A B f l; case l; clear l. intros l1 l2 H; exists nil; exists nil. revert H; case l1; clear l1. case l2; clear l2. intros _; repeat split; apply eq_refl. intros b2 l2 H; discriminate. intros b1 l1 H; discriminate. intros a l l1; case l1; clear l1. intros l2 H; exists nil; exists (a :: l); repeat split; trivial. intros b1 l1 l2 H; injection H; clear H; intros H H'. destruct (split_map_set A B f l l1 l2 H) as [k1 [k2 [H1 [H2 H3]]]]. exists (a :: k1); exists k2; repeat split; trivial. simpl; apply f_equal; assumption. simpl; rewrite H'; rewrite H2; apply eq_refl. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)