mathlib

9015d2ad - refactor(set_theory/game/pgame): Redefine `subsequent` (#13752)

refactor(set_theory/game/pgame): Redefine `subsequent` (#13752) We redefine `subsequent` as `trans_gen is_option`. This gives a much nicer induction principle than the previous one, and allows us to immediately prove well-foundedness.