proposition: Lemma omniscient_rel_choice : forall A B (R : A->B->Prop), exists R', rel_incl R' R /\ forall x, (exists y, R x y) -> (exists! y, R' x y).
proof: Proof. Proof using. intros. apply~ guarded_rel_choice. Qed.
imports: TLC(LibTactics LibLogic LibEpsilon LibRelation)