basic): use `subtype p` not `coe_sort (set_of p)` (#9559)

Commit

4 years ago

fix(data/equiv/basic): use `subtype p` not `coe_sort (set_of p)` (#9559) `↥{x | p x}` is just a clumsy way to write `{x // p x}`.

Author

eric-wieser

Parents