proposition: Lemma eqrxP X1 X2 : reflect (X1 = X2) (eqrx X1 X2).
proof: Proof. apply: (iffP idP)=> [|<-]; last by rewrite /eqrx decT. rewrite /eqrx; case: (dec _)=> //= eqv h. by case: X1 X2 eqv => [X1] [X2] /= eqv; rewrite (@pex _ X1 X2). Qed.
imports: mathcomp(all_ssreflect all_algebra) Setoid