Stream: MetaCoq

Topic: wf_universes and reduction

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Nov 18 2020 at 11:59):

Not yet no, I didn't need it

Last updated: Jun 13 2024 at 03:02 UTC