proposition: Lemma exists_map12_without_repetition : forall A B (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, None) => False | (Some b, None) => P b | (None, Some c) => P c | (Some b, Some c) => P b \/ P c end) -> (exists d, In d (map12_without_repetition eq_bool f l) /\ P d)).
proof: Proof. intros A B eq_bool eq_bool_ok P f; fix exists_map12_without_repetition 1; intro l; case l; clear l. intros [a [a_in_nil _]]; contradiction. intros a l; assert (IH := exists_map12_without_repetition l). intros [a0 [[a0_eq_a | a0_in_l] H]]. subst a0; simpl; revert IH; case l; clear l. intros _; revert H; destruct (f a) as [[b' | ] [b'' | ]]. intros [Pb' | Pb'']. exists b'; split; [left; reflexivity | assumption]. exists b''; split; [right; left; reflexivity | assumption]. intros Pb'; exists b'; split; [left; reflexivity | assumption]. intros Pb''; exists b''; split; [left; reflexivity | assumption]. contradiction. intros a2 l IH. generalize (eq_bool_ok a a2); case (eq_bool a a2); [intro a_eq_a2 | intro a_diff_a2]. apply IH; exists a; split; [left; symmetry | idtac]; assumption. revert H; destruct (f a) as [[b' | ] [b'' | ]]. intros [Pb' | Pb'']. exists b'; split; [left; reflexivity | assumption]. exists b''; split; [right; left; reflexivity | assumption]. intros Pb'; exists b'; split; [left; reflexivity | assumption]. intros Pb''; exists b''; split; [left; reflexivity | assumption]. contradiction. destruct IH as [d [d_in_map Pd]]. exists a0; split; assumption. exists d; split; [idtac | assumption]. revert d_in_map; simpl; case l; clear a0_in_l l. contradiction. intros a2 l; case (eq_bool a a2). intro; assumption. destruct (f a) as [[b' | ] [b'' | ]]. intro; do 2 right; assumption. intro; right; assumption. intro; right; assumption. intro; assumption. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)