Bug 27 closed now that universe contexts can be refined during the proof,
here instantiating a flexible level with Set.