Commit 2021-01-27 18:19 4cc0d525
View on Github →refactor(data/set/basic): simpler proofs (#5920)
This replaces many uses of simp
and finish
with direct term proofs
to speed up the overall compilation of the file.
This PR is WIP in the sense that not all of set.basic
is converted,
but there are no dependencies between the changes so this can be merged
at any point.