return to top
source
NF weak partition development: CompactSyntaxFVDisable.
Disable the legacy global simp registration; use explicit FV lemmas.