proposition: Lemma exists_map12_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, None) => False | (None, Some f2_a) => P f2_a | (Some f1_a, None) => P f1_a | (Some f1_a, Some f2_a) => P f1_a \/ P f2_a end) -> (exists b, In b (map12_without_repetition eqA f l) /\ P b)).
proof: Proof. intros A B eqA P f; induction l as [ | a1 l]. intros [a [In_a _]]; contradiction. destruct l as [ | a2 l]. intros [a [[Eq_a_a1 | In_a] P_f_a]]; simpl. subst a; destruct (f a1) as [o1 o2]; destruct o1 as [f1_a1 | ]; destruct o2 as [f2_a1 | ]. generalize P_f_a; clear P_f_a; intros [P_f1_a1 | P_f2_a1]. exists f1_a1; intuition. exists f2_a1; intuition. exists f1_a1; intuition. exists f2_a1; intuition. contradiction. contradiction. intros [a [[Eq_a_a1 | In_a] P_f_a]]. subst a; simpl; elim (eqA a1 a2). intro; subst a1; apply IHl; exists a2; intuition. destruct (f a1) as [o1 o2]; destruct o1 as [f1_a1 | ]; destruct o2 as [f2_a1 | ]. generalize P_f_a; clear P_f_a; intros [P_f1_a1 | P_f2_a1]. exists f1_a1; intuition. exists f2_a1; intuition. exists f1_a1; intuition. exists f2_a1; intuition. contradiction. assert (Hrec : exists b : B, In b (map12_without_repetition eqA f (a2 :: l)) /\ P b). apply IHl; exists a; split; trivial. generalize Hrec; intros [b [In_b P_b]]; exists b; split; trivial. simpl; elim (eqA a1 a2). intro; subst a1; trivial. intros _; destruct (f a1) as [o1 o2]; destruct o1 as [P_f1_a1 | ]; destruct o2 as [P_f2_a1 | ]. right; right; trivial. right; trivial. right; trivial. trivial. Qed.
imports: List Arith