proposition: Lemma mem_bool_app : forall x l1 l2, (mem_bool eq_bool x (l1++l2)) = orb (mem_bool eq_bool x l1) (mem_bool eq_bool x l2).
proof: Proof. intros x l1. functional induction (mem_bool eq_bool x l1). simpl;reflexivity. simpl. intros l2;rewrite IHb0. auto with bool. Qed.
imports: CoLoR(more_list decidable_set list_set) Coq(List Lia FunInd)