proposition: Theorem list_choice : forall (A B : Type)(eqd : forall (a1 a2 : A), {a1 = a2} + {a1 <> a2}) P (ls : list A) (b : B), (forall a, In a ls -> exists (b : B), P a b) -> exists (f : A -> B), (forall a, In a ls -> P a (f a)).
proof: Proof. induction ls; intuition. exists (fun a => b). intuition. simpl in *. intuition. edestruct (H a); intuition. edestruct (H0); intuition. exists (fun a0 => if (eqd a a0) then x else (x0 a0)). intuition. inversion H3; clear H3; subst. destruct (eqd a0 a0); intuition. destruct (eqd a a0); intuition. subst. trivial. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1