proposition: Lemma exists_map_without_repetition : forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) (P : B -> Prop) f l, (exists a, In a l /\ match f a with | None => False | Some f_a => P f_a end) -> (exists b, In b (map_without_repetition eqA f l) /\ P b).
proof: Proof. intros A B eqA P f. assert (In_map_right : forall b a l, In b (map_without_repetition eqA f l) -> In b (map_without_repetition eqA f (a :: l))). intros b a1 l In_b; simpl; destruct l as [ | a2 l]. contradiction. elim (eqA a1 a2); trivial; destruct (f a1) as [ b1 | ]; trivial; intros _; right; trivial. induction l as [ | a1 l]. intros [a [In_a _]]; contradiction. intros [a [[Eq_a_a1 | In_a] P_f_a]]. simpl; subst a1; destruct l as [ | a2 l]; intuition. destruct (f a) as [b | ]; [ exists b; intuition | contradiction ]. elim (eqA a a2). intro; subst a; apply IHl; exists a2; intuition. intros _; destruct (f a) as [ b | ]; [exists b; intuition | contradiction]. assert (H: exists b : B, In b (map_without_repetition eqA f l) /\ P b). apply IHl; exists a; intuition. generalize H; intros [b H_b]; exists b; intuition. Qed.
imports: List Arith