proposition: Lemma change_in : forall order f l, In f l -> more_list.mem_bool eq_bool f (qs order (remove_red l)) = true.
proof: Proof. intros order f l H. apply (more_list.in_impl_mem (@eq A) (fun a => eq_refl a)) in H. apply XSet.remove_red_included in H. generalize (more_list.mem_bool_ok _ _ eq_bool_ok f (remove_red l)). case_eq (more_list.mem_bool eq_bool f (remove_red l)). clear H;intros H _. 2:clear -H;intros _ abs;contradiction. rewrite (qs_valid order) in H. exact H. Qed.
imports: CoLoR(more_list decidable_set list_set) Coq(List Lia FunInd)