proposition: Lemma mem_map_set : forall (A B : Type) eqB eqB_bool (eqB_bool_ok : forall a1 a2, match eqB_bool a1 a2 with true => eqB a1 a2 | false => ~ eqB a1 a2 end) (f : A -> B) b l, mem eqB b (map f l) -> {a : A | eqB b (f a) /\ In a l}.
proof: Proof. intros A B eqB eqB_bool eqB_bool_ok f b; induction l as [ | a1 l]. contradiction. generalize (eqB_bool_ok b (f a1)); case (eqB_bool b (f a1)); [intro b_eq_fa1 | intro b_diff_fa1]. intros _; exists a1; split; [assumption | left; apply eq_refl]. simpl; intro b_in_fa1_fl. destruct IHl as [a [fa_eq_b a_in_l]]. destruct b_in_fa1_fl as [fa1_eq_b | b_in_fl]; [apply False_rect; apply b_diff_fa1 | idtac]; assumption. exists a; split; [assumption | right; assumption]. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)