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