RecordUpdatePreservesType.agda:18,14-17 R !=< Q of type Set when checking that the expression old has type Q