proposition: Lemma split_all_is_sound : forall (A : Type) (l : list A) b l' l'', In (b,(l',l'')) (split_all l) <-> l = l' ++ b :: l''.
proof: Proof. intros A l; induction l as [ | a l]; intros b l' l''. split; intro H. contradiction. destruct l'; discriminate. simpl; split; intro H. rewrite in_map_iff in H; destruct H as [ H | H ]. injection H; intros; subst; trivial. destruct H as [[c [k' k'']] [H H']]. injection H; intros; subst. simpl; apply (f_equal (fun l => a :: l)). rewrite <- (IHl b k' l''); trivial. rewrite in_map_iff; destruct l' as [ | a' l']; simpl in H; injection H; intros; subst. left; trivial. right; exists (b,(l',l'')); split; trivial. rewrite (IHl b l' l''); trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)