 In practice, CRM splits naturally into two parts. In the first of these, we consider a theorem \(T\) of INT or RUSS, and try to find some principle, valid in that model and other than \(T\) itself, whose addition to BISH is necessary and sufficient for a constructive proof of \(T\). In the second part of CRM we deal with a theorem \(T\) of CLASS that we suspect is nonconstructive, and we try to prove that \(T\) is equivalent, over BISH, to one of a number of known essentially-nonconstructive principles, such as MP, LLPO, LPO, or LEM. For an example of this part of CRM, we mention our earlier proof that the classical least-upper-bound principle implies, and hence is equivalent to, LEM. 