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.
Not yet no, I didn't need it
Last updated: Sep 26 2023 at 12:02 UTC