proposition: Lemma in_split : forall (A : Type) (a : A) (l : list A), In a l -> exists l1, exists l2, l = l1 ++ a :: l2.
proof: Proof. intros A a l; induction l as [ | e l]. contradiction. intros [a_eq_e | a_in_l]. subst e. exists (@nil A); exists l; trivial. destruct (IHl a_in_l) as [l' [l'' H]]. exists (e :: l'); exists l''; subst l; simpl; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)