TODO: One day move to Staerk-et-al's \"Set of object types\" instead of \"wider\" object types
created during the verification.
\"Wider\" object types don't allow us to check for things like that below.