proposition: Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice : RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice.
proof: Proof. intros rel_choice proof_irrel. red; intros A B P R H. destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as (R',(HR'R,H0)). - intros (x,HPx). destruct (H x HPx) as (y,HRxy). exists y; exact HRxy. - set (R'' := fun (x:A) (y:B) => exists H : P x, R' (existT P x H) y). exists R''; split. + intros x y (HPx,HR'xy). change x with (projT1 (existT P x HPx)); apply HR'R; exact HR'xy. + intros x HPx. destruct (H0 (existT P x HPx)) as (y,(HR'xy,Huniq)). exists y; split. * exists HPx; exact HR'xy. * intros y' (H'Px,HR'xy'). apply Huniq. rewrite proof_irrel with (a1 := HPx) (a2 := H'Px); exact HR'xy'. Qed.
imports: RelationClasses Logic