proposition: Lemma prop_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, (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 eq_bool f l) -> P b).
proof: Proof. intros A B eq_bool eq_bool_ok P f; fix prop_map_without_repetition 1; intro l; case l; clear l; simpl. intros _ b b_in_nil; contradiction. intros a l IH; generalize (prop_map_without_repetition l (tail_prop _ IH)); revert IH. case l; clear l. intros IH H b; generalize (IH a (or_introl _ (eq_refl _))); case (f a). simpl; intros b' Pb' [b_eq_b' | b_in_nil]. subst b'; assumption. contradiction. intros _ b_in_nil; contradiction. intros a2 l IH H b; generalize (eq_bool_ok a a2); case (eq_bool a a2); [intro a_eq_a2 | intro a_diff_a2]. apply H. generalize (IH a (or_introl _ (eq_refl _))); case (f a). simpl In; intros b' Pb' [b_eq_b' | b_in_mapl]. subst b'; assumption. apply H; assumption. intros _; apply H. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)