 An element of this type \(B\) is thereby a pair consisting of a convergent sequence \(\bx\) of rationals and a proof \(p\) that it is convergent. A suitable equivalence relation \({\sim}\) on \(R\) is defined by taking \((x,p)\sim(y,q)\) to mean