Commit 2022-06-20 13:49 66d3f897

feat(logic/unique): functions from a unique type is const (#14823)

• A function f from a unique type is equal to the constant function with value f default, and the analogous heq version for dependent functions.
• Also changes Π a : α, Sort v in the file to α → Sort v. Inspired by https://github.com/leanprover-community/mathlib/pull/14724#discussion_r900542203