Commit 2022-04-26 01:09 24a8bb93
View on Github →feat(order/well-founded): Remove redundant arguments (#13702)
All of these are inferred as {α : Type*} (as opposed to {α : Sort*}), and there is already a variables {α : Type*} at the top of the file.