proposition: Lemma guarded_rel_choice : forall A B (P : A->Prop) (R : A->B->Prop), (forall x, P x -> exists y, R x y) -> (exists R', rel_incl R' R /\ forall x, P x -> exists! y, R' x y).
proof: Proof. Proof using. intros. destruct (rel_choice (fun (x:sig P) (y:B) => R (sig_val x) y)) as (R',(HR'R,M)). intros (x,HPx). destruct (H _ HPx) as (y,HRxy). exists~ y. set (R'' := fun (x:A) (y:B) => exists (H : P x), R' (exist P x H) y). exists R''. split. intros x y (HPx,HR'xy). apply (HR'R _ _ HR'xy). intros x HPx. destruct (M (exist P x HPx)) as (y,(HR'xy,Uniq)). exists y. split. exists~ HPx. intros y' (H'Px,HR'xy'). apply Uniq. rewrite~ (proof_irrelevance HPx H'Px). Qed.
imports: TLC(LibTactics LibLogic LibEpsilon LibRelation)