(* Nijmegen expects redefinition of sorts *)
Definition CProp := Prop.
Record test : CProp := { n:nat }.