Commit 2022-07-12 12:46 2bca4d61
View on Github →chore(set_theory/ordinal/cantor_normal_form): mark CNF as pp_nodot (#15228)
b.CNF o doesn't make much sense, since b is the base argument rather than the main argument.
The existing lemmas all use the CNF b o spelling anyway.