In this first version, functions and properties of these functions are left in separate variables and hypotheses. As a result, the extracted code is slightly more readable, and some of the proofs are easier because, we don't have any problems with implicit arguments (see explanation in the next section.
In this version we define, orders, complete preorders, and so on as canonical structures. We then define types of monotonic and continuous functions as records containing a function a proofs about this function. Again, this is made into a canonical structure. Proofs need to be arrange according to the hierarchy of structures (a continuous function is a monotonic function with extra properties), and sometimes rewriting fails because implicit arguments (which are not visible) have different shapes in goals and in hypotheses, although they are convertible. Aside from that, all proofs proceed as in the previous section.