Record C (A: Type) : Type := { f: A }.
Existing Class C.