proposition: Lemma mem_split_set : forall a l, mem a l -> {a' : A & {l' : list A & {l'' : list A | eqA a a' /\ l = l' ++ a' :: l'' /\ remove a l = Some (l' ++ l'')}}}.
proof: Proof. intros a l a_mem_l; generalize (in_remove a l); case (remove a l). intros l' H; exact H. intro a_not_mem_l; absurd (mem a l); assumption. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)