proposition: Lemma in_map_set : forall (A B : Type) (eqB_dec : forall b1 b2 : B, {b1 = b2}+{b1 <> b2}) (f : A -> B) b l, In b (map f l) -> {a : A | f a = b /\ In a l}.
proof: Proof. intros A B eqB_dec f b; induction l as [ | a1 l]. contradiction. destruct (eqB_dec b (f a1)) as [b_eq_fa1 | b_diff_fa1]. intros _; exists a1; split; [apply sym_eq; 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; apply sym_eq | idtac]; assumption. exists a; split; [assumption | right; assumption]. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)