Commit 2022-02-23 13:18 c5267895

feat(set_theory/ordinal_arithmetic): is_normal.eq_iff_zero_and_succ (#12222) Two normal functions are equal iff they're equal at 0 and successor ordinals. This is used for a few lemmas in #12202.