ZF_finite.Not_regular_model