Make OFE.hom an explicit subtype

OFE.hom is a subtype. #177  (merging soon) adds nonexpansive coercions to and from the subtype to the CMRA on OFE.hom, indicating that these constructions may be redundant. 

```
def Hom.toSubtype [OFE α] [OFE β] (f : α -n> β) : { f : α → β // NonExpansive f }
def Hom.ofSubtype [OFE α] [OFE β] (f : { f : α → β // NonExpansive f }) : α -n> β
```