Commit 2021-08-28 19:59 d75a2d96
View on Github →refactor(data/set/finite): use [fintype (plift ι)] in finite_Union (#8872)
This way we can use finite_Union instead of finite_Union_Prop.
refactor(data/set/finite): use [fintype (plift ι)] in finite_Union (#8872)
This way we can use finite_Union instead of finite_Union_Prop.