[ refactor ] generalise inclusion between Propositional permutation, and arbitrary Setoid-based version on same carrier#2709