proposition: Lemma omniscient_functional_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. apply~ guarded_functional_choice. Qed.
imports: TLC(LibTactics LibLogic LibEpsilon LibRelation)