5.3 Mode change

For mode change, we use the word reconsider to conduct a mode change. (cf.4.10).

     reconsider U=D as Nat by ...;


    As shown above, by using reconsider, it is possible to change D of Real's mode to U of Nat's mode.