Meven Lennon-Bertrand (Nov 18 2020 at 11:31): Meven Lennon-Bertrand (Nov 18 2020 at 11:31):Is it proven somewhere that wf_universes is preserved by reduction? I can’t find it either in PCUICReduction of PCUICWfUniverses, but I guess it might be hidden somewhere else… On a well-typed term, this can of course be proven as a consequence of SR, but I’m wondering if the syntactical property is already somewhere.
Matthieu Sozeau (Nov 18 2020 at 11:59):Not yet no, I didn't need it
Last updated: Jun 01 2023 at 11:01 UTC