Commit 2021-10-13 15:48 f29755b9

refactor(data/set/pairwise): generalize pairwise_disjoint to semilattice_inf_bot (#9670) set.pairwise_disjoint was only defined for set (set α). Now, it's defined for set α where semilattice_inf_bot α. I also

• move it to data.set.pairwise because it's really not about set anymore.
• drop the set namespace.
• add more general elimination rules and rename the current one to elim_set.