Stop using lbound:Prop

[SkySkimmer]

Depends:

• retype template poly as though sort poly restricted to above_prop  #19970
• pretype template poly as though sort poly restricted to above_prop #19964

Overlays:

• Adapt to coq/coq#19985 (template poly has pseudo sort poly) ejgallego/rocq-lsp#893
• Adapt to coq/coq#19985 (template poly has pseudo sort poly) rocq-community/paramcoq#133
• Adapt to coq/coq#19985 (template poly has pseudo sort poly) rocq-community/rocq-lean-import#22

[coqbot-app]

🔴 CI failure at commit 02cd67a without any failure in the test-suite

✔️ Corresponding job for the base commit 253e9af succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-riscv_coq

• You can also pass me a specific list of targets to minimize as arguments.

[SkySkimmer]

Minimized error from riscv

Unset Universe Minimization ToSet.
Record R (T:Type) := mk { x : nat -> T }.

[SkySkimmer]

Minimized error from riscv

The higher layers see Type@{q|u} -> Type@{q|u}, but the kernel is not actually sort polymorphic so it sees the constructor argument (nat -> T) : Type@{max(Set,u)} and wants Type@{u} -> Type@{max(Set,u)}

[SkySkimmer]

"is pseudo sort poly" should probably be an annotation for each template universe instead of being global to the inductive, for strange types like

Inductive dumb' (A:Type) (b:bool) (B : Type) := cons' : A -> (b = true -> dumb' A false nat) -> dumb' A b B.

(the univ of A is pseudo sort poly, the univ of B is not but is not used in the conclusion)

[SkySkimmer]

Minimized error from riscv

The higher layers see Type@{q|u} -> Type@{q|u}, but the kernel is not actually sort polymorphic so it sees the constructor argument (nat -> T) : Type@{max(Set,u)} and wants Type@{u} -> Type@{max(Set,u)}

Trying to work around this seems difficult, so I guess I'll try to make the kernel more sort polymorphic in this PR.

[ppedrot]

@coqbot merge now

[coqbot-app]

@ppedrot: Please take care of the following overlays:

• 19985-SkySkimmer-cominductive-lbound.sh