proposition: Lemma split_mem_bool : forall x y l l1 l2, split l x = (l1,l2) -> mem_bool eq_bool y l = orb (mem_bool eq_bool y l1) (mem_bool eq_bool y l2).
proof: Proof. intros x y l; functional induction (split l x); intros l1' l2' H;injection H;clear H;intros h1 h2;subst;simpl. reflexivity. rewrite IHp with (1:=e0);auto with bool. rewrite IHp with (1:=e0);auto with bool. case (eq_bool y y0);case (mem_bool eq_bool y l1'); case (mem_bool eq_bool y l2); reflexivity. Qed.
imports: CoLoR(more_list decidable_set list_set) Coq(List Lia FunInd)