Dear Coq Discourse,

I have a question about instantiating Polymorphic universes, in particular how discharge/remove one universe from a definition and set it to a universe level that depends on the others. question is as follows:

# Question

Suppose I have a lemma of the form:

```
MyLemma@{a b c} : Mysort {a b c |= a < c b <= c}
```

where the universe c comes from some definitions that are made due to the internals of the theory that I am writing. For the type I want to instantiate, c’s universe level does not matter, and I need it gone for it to be correct w.r.t. to a module type’s definitions for the module which `MyLemma`

will instantiate a Parameter of.

My first naive attempt at a solution is the following, to make a *dummy* lemma that gets rid of y as follows:

`MyLemma'@{a b} :=MyLemma@{a b max(a+1,b)}`

If this was allowed my problem is solved immediately. However, I get the following error `Syntax error: [univ_level_or_quality] or '|' or '}' expected (in [univ_annot]).`

, so it seems that this way of specifying universes is not allowed in Coq.

I have also tried a tricksy way of solving this problem by loading the required universe into *dummy* arguments, i.e. doing something like the following to pull in the correct universe:

```
Definition y@{a b c}:=(fun (A:Type@{a}) (B:Type@{b}) (C:Type@{c}) => Type@{c}).
Definition g@{a b} := (fun (A:Type@{a}) (B:Type@{b}) (C:Type@{max(a+1,b)}) => (y@{a b _} A B C) ).
```

However in this instance I get an (expected) universe unbound error. I tried finagling it a little to get it to work but could not.

Lastly I have tried looking into the docs on this issue but didn’t really get all that in the way of understanding all that was said there. I did look and see that there is some thing called ` Private Polymorphic Universes`

which looked at least in the same ball park as what I’m trying to achive - though I couldn’t figure out how to use it or if I want to opaque the lemmas in the first place.

Does Coq have any mechanism to solve the problem I am experiencing, otherwise it means I will have to bake lots of nonsensical random universe levels into my module types in a way that is ultimately brittle and unnecessary?