proposition: Lemma qs_valid : forall f l, more_list.mem_bool eq_bool f l = more_list.mem_bool eq_bool f (qs l).
proof: Proof. intros f l. functional induction (qs l). reflexivity. simpl. rewrite mem_bool_app. simpl. rewrite <- IHl0. rewrite <- IHl1. rewrite split_mem_bool with (1:=e0). case (eq_bool f x);case (mem_bool eq_bool f l1); case (mem_bool eq_bool f l2); reflexivity. Qed.
imports: CoLoR(more_list decidable_set list_set) Coq(List Lia FunInd)