take C = uReal . 0; :: thesis: C is *real
thus C is *real ; :: thesis: verum