proposition: Lemma exists_map_without_repetition : forall (A B : Type) (eq_bool : A -> A -> bool) (eq_bool_ok :forall a1 a2 : A, match eq_bool a1 a2 with true => a1 = a2 | false => a1 <> a2 end) (P : B -> Prop) f l, (exists a, In a l /\ match f a with | None => False | Some b => P b end) -> (exists b, In b (map_without_repetition eq_bool f l) /\ P b).
proof: Proof. intros A B eq_bool eq_bool_ok P f; fix exists_map_without_repetition 1; intro l; case l; clear l; simpl. intros [a [F _]]; contradiction. intros a l; generalize (exists_map_without_repetition l). case l; clear l. intros _ [a' [[a_eq_a' | a'_in_nil] H2]]. subst a'; revert H2; case (f a). intros b Pb; exists b; split; [left; reflexivity | assumption]. contradiction. contradiction. intros a2 l IH H; generalize (eq_bool_ok a a2); case (eq_bool a a2); [intro a_eq_a2 | intro a_diff_a2]. apply IH. destruct H as [a' [[a_eq_a' | a'_in_a2l] H]]. subst a' a2; exists a; split; [left; reflexivity | assumption]. exists a'; split; assumption. destruct H as [a' [[a_eq_a' | a'_in_a2l] H]]. subst a'; revert H; case (f a). intros b Pb; exists b; split; [left; reflexivity | assumption]. contradiction. destruct IH as [b [b_in_map Pb]]. exists a'; split; assumption. exists b; split; [case (f a) | assumption]. intros b'; right; assumption. assumption. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)