Commit 2022-06-10 02:04 ed2cfce8

feat(set_theory/ordinal/basic): tweak theorems on order type of empty relation (#14650) We move the theorems on the order type of an empty relation much earlier, and golf them. We also remove other redundant theorems. zero_eq_type_empty is made redundant by type_eq_zero_of_empty, while zero_eq_lift_type_empty is made redundant by the former lemma and lift_zero.