Commit 2023-08-21 00:12 782e4d39
View on Github →feat(Data/List/Chain): well-foundedness of chains under List.Lex (#6432)
shorter proof of the main result of #6361
Zulip: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/List.2ELex.20is.20well.20founded.20on.20decreasing.20lists/near/382708025