proposition: Theorem singleton_choice : forall (A : Type) (P : A->Prop), (exists x : A, P x) -> exists P' : A->Prop, subset P' P /\ exists! x, P' x.
proof: Proof. intros A P H. destruct (relational_choice unit A (fun _ => P) (fun _ => H)) as (R',(Hsub,HR')). exists (R' tt); firstorder. Qed.
imports: ClassicalUniqueChoice RelationalChoice ChoiceFacts