Commit 2022-05-04 07:50 9015d2ad
View on Github →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.