proposition: Lemma rel_choice : forall A B (R:A->B->Prop), (forall x, exists y, R x y) -> (exists R', rel_incl R' R /\ forall x, exists! y, R' x y).
proof: Proof. Proof using. introv H. destruct~ (functional_choice R) as [f Hf]. exists (fun x y => f x = y). split. introv E. simpls. subst~. intros x. exists~ (f x). Qed.
imports: TLC(LibTactics LibLogic LibEpsilon LibRelation)