finite): use `[fintype (plift ι)]` in `finite_Union` (#8872)

Commit

4 years ago

refactor(data/set/finite): use `[fintype (plift ι)]` in `finite_Union` (#8872) This way we can use `finite_Union` instead of `finite_Union_Prop`.

Author

urkud

Parents