feat(data/set/basic): pairwise_on.imp_on (#7578)
Provide more helper lemmas for transferring `pairwise_on` between different relations. Provide a rephrase of `pairwise_on.mono'` as `pairwise_on.imp`.
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
