Class C.
Parameter P: C -> Prop.
Fail Record R: Type := { _: C; u: P _ }.