Many details of the proof will need intuitionizing.
The statement of the theorem probably will also need some
change (for example, I suppose the elements of ran ( RR _D F )
need to be apart from zero rather than merely not equal).
Perhaps the easiest way to approach this is going to be
to intuitionize set.mm
working forward starting from dvmptsub (which is the end
of where the derivatives have apparently been intuitionized),
seeing what can be intuitionized and what changes are needed.
Either dvcnvre will fall out of this process or it will be
more clear what its dependencies will be.