Is it known that subject reduction in Coq is broken in the presence of SProp?
This one is for @Gaëtan Gilbert
Reported as https://github.com/coq/coq/issues/14015
Last updated: Jun 04 2023 at 19:30 UTC