proposition: Lemma omniscient_functional_unique_choice : forall A `{Inhab B} (R : A->B->Prop), exists f, forall x, (exists! y, R x y) -> R x (f x).
proof: Proof. Proof using. intros. destruct (omniscient_functional_choice R) as [f F]. exists f. introv (y&Hy&Uy). autos*. Qed.
imports: TLC(LibTactics LibLogic LibEpsilon LibRelation)