proposition: Lemma in_split_set : forall (A : Type) (eq_bool : A -> A -> bool) (eq_bool_ok : forall a1 a2 : A, match eq_bool a1 a2 with true => a1 = a2 | false => a1 <> a2 end) (a : A) (l : list A), In a l -> {l1 : list A & { l2 : list A | l = l1 ++ a :: l2}}.
proof: Proof. intros A eq_bool eq_bool_ok a l; induction l as [ | e l]. contradiction. generalize (eq_bool_ok e a); case (eq_bool e a); [intro e_eq_a | intro e_diff_a]. intros _; exists (@nil A); exists l; simpl; subst; trivial. intro a_in_el; destruct IHl as [l' [l'' H]]. destruct a_in_el as [e_eq_a | a_in_l]; trivial. absurd (e = a); trivial. exists (e :: l'); exists l''; subst l; simpl; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)