Commit 2021-01-27 08:41 e9a1e2b3
View on Github →refactor(data/pequiv): simpler proof of pequiv.of_set_univ (#5907)
17X smaller proof
co-authors: lean-gptf, Stanislas Polu
refactor(data/pequiv): simpler proof of pequiv.of_set_univ (#5907)
17X smaller proof
co-authors: lean-gptf, Stanislas Polu