proposition: Lemma proof_irrel_rel_choice_imp_eq_dec' : a1=a2 \/ ~a1=a2.
proof: Proof. assert (decide: forall x:A, x=a1 \/ x=a2 -> exists y:bool, x=a1 /\ y=true \/ x=a2 /\ y=false). - intros a [Ha1|Ha2]; [exists true | exists false]; auto. - assert (guarded_rel_choice := rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrelevance). destruct (guarded_rel_choice A bool (fun x => x=a1 \/ x=a2) (fun x y => x=a1 /\ y=true \/ x=a2 /\ y=false)) as (R,(HRsub,HR)). + apply decide. + destruct (HR a1) as (b1,(Ha1b1,_Huni1)). * left; reflexivity. * destruct (HRsub a1 b1 Ha1b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)]. -- destruct (HR a2) as (b2,(Ha2b2,Huni2)). ++ right; reflexivity. ++ destruct (HRsub a2 b2 Ha2b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)]. ** left; symmetry; assumption. ** right; intro H. subst b1; subst b2; subst a1. assert (false = true) by auto using Huni2, Ha1b1. discriminate. -- left; assumption. Qed.