[Merged by Bors] - chore(Order/RelIso/Basic): [s : Setoid α] => {s : Setoid α}

[Merged by Bors] - chore(Order/RelIso/Basic): [s : Setoid α] => {s : Setoid α} #22772