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.