proposition: Lemma prop_map_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 => True | Some f_a => P f_a end) -> (forall b, In b (map_without_repetition eqA f l) -> P b).
proof: Proof. induction l as [ | a1 l]. contradiction. assert (In_a1 : In a1 (a1 :: l)). left; trivial. intros H; generalize (H a1 In_a1); simpl; destruct l as [ | a2 l]. destruct (f a1) as [ f_a1 | ]; simpl; intuition; subst; trivial. elim (eqA a1 a2); intro eq_a1_a2. intros; apply IHl; trivial; intros; apply H; right; trivial. destruct (f a1) as [ f_a1 | ]. intros P_f_a1 b [eq_f_a1_b | In_b]. subst; apply P_f_a1; left; trivial. apply IHl; trivial; intros; apply H; right; trivial. intros; apply IHl; trivial; intros; apply H; right; trivial. Qed.
imports: List Arith