proposition: Lemma prop_map12_without_repetition : forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) (P : B -> Prop) f l, (forall a, In a l -> match f a with | (None, None) => True | (Some f1_a, None) => P f1_a | (None, Some f2_a) => P f2_a | (Some f1_a, Some f2_a) => P f1_a /\ P f2_a end) -> (forall b, In b (map12_without_repetition eqA f l) -> P b).
proof: Proof. intros A B eqA P f; induction l as [ | a1 l]. contradiction. assert (In_a1 : In a1 (a1 :: l)). left; trivial. intros H b; assert (Hrec : forall b : B, In b (map12_without_repetition eqA f l) -> P b). intros; apply IHl; trivial; intros; apply H; right; trivial. clear IHl; simpl; generalize (H a1 In_a1). destruct l as [ | a2 l]. destruct (f a1) as [o1 o2]; destruct o1 as [ f1_a1 | ]; destruct o2 as [ f2_a1 | ]; [ intros [P_f1_a1 P_f2_a1] | intros P_f1_a1 | intros P_f2_a1 | idtac]. intros [Eq_b_f1_a1 | [Eq_b_f2_a1 | In_b]]; subst; trivial; contradiction. intros [Eq_b_f1_a1 | In_b]; subst; trivial; contradiction. intros [Eq_b_f2_a1 | In_b]; subst; trivial; contradiction. contradiction. elim (eqA a1 a2). intros; apply Hrec; trivial. destruct (f a1) as [o1 o2]; destruct o1 as [ f1_a1 | ]; destruct o2 as [ f2_a1 | ]; [ intros _ [P_f1_a1 P_f2_a1] | intros _ P_f1_a1 | intros _ P_f2_a1 | intros _]. intros [Eq_b_f1_a1 | [Eq_b_f2_a1 | In_b]]; subst; trivial; apply Hrec; trivial. intros [Eq_b_f1_a1 | In_b]; subst; trivial; apply Hrec; trivial. intros [Eq_b_f2_a1 | In_b]; subst; trivial; apply Hrec; trivial. intros; apply Hrec; trivial. Qed.
imports: List Arith